siman

Theorem.

Arguments:

phi (pr), psi (pr),

Hypotheses:

(phiwedgepsi)

Assertions:

psi
phi

Proof:

Hyp Ref Line Expr
Hypo1(phiwedgepsi)
siman<2((phiwedgepsi)tophi)
siman>3((phiwedgepsi)topsi)
1, 2ax-mp4phi
1, 3ax-mp5psi