pm3.4

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

((phiwedgepsi)to(phitopsi))

Proof:

Hyp Ref Line Expr
siman>1((phiwedgepsi)topsi)
1ax12((phiwedgepsi)to(phitopsi))