jct<

Theorem.

Arguments:

phi (pr), psi (pr),

Hypotheses:

psi

Assertions:

(phito(psiwedgephi))

Proof:

Hyp Ref Line Expr
Hypo1psi
1ax12(phitopsi)
id3(phitophi)
2, 3jca4(phito(psiwedgephi))