exp

Theorem.

Arguments:

phi (pr), psi (pr), chi (pr),

Hypotheses:

((phiwedgepsi)tochi)

Assertions:

(phito(psitochi))

Proof:

Hyp Ref Line Expr
Hypo1((phiwedgepsi)tochi)
impexp2(((phiwedgepsi)tochi)leftrightarrow(phito(psitochi)))
2bi>3(((phiwedgepsi)tochi)to(phito(psitochi)))
1, 3ax-mp4(phito(psitochi))