al.imdi

Theorem.

Arguments:

x (sv), phi (pr), psi (pr),

Assertions:

(forallx(phitopsi)to(forallxphitoforallxpsi))

Proof:

Hyp Ref Line Expr
ax41(forallxphitophi)
1syl>2((phitopsi)to(forallxphitopsi))
2ax43(forallx(phitopsi)to(forallxphitopsi))
3ax54(forallx(phitopsi)toforallx(forallxphitopsi))
ax55(forallx(forallxphitopsi)to(forallxphitoforallxpsi))
4, 5syl6(forallx(phitopsi)to(forallxphitoforallxpsi))