Theorem com4t 40

Description: Commutation of antecedents. Rotate twice.

Hypothesis

Ref	Expression
com4.1	|- (ph -> (ps -> (ch -> (th -> ta))))

Assertion

Ref	Expression
com4t	|- (ch -> (th -> (ph -> (ps -> ta))))

Proof of Theorem com4t

Step	Hyp	Ref	Expression
1		com4.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	com4l 39	. 2 |- (ps -> (ch -> (th -> (ph -> ta))))
3	2	com4l 39	1 |- (ch -> (th -> (ph -> (ps -> ta))))

Syntax hints:   -> wi 3

This theorem is referenced by:  com4r 41  mopick 1431  tfindsg 3157  isofrlem 3892  tfr3 3917  pssnn 4519  aceq5 4720  ltexprlem7 5128  bccl2t 6917  clm4le 7027  caucvglem4 7104  infxpidmlem11 7513  retopbas 7605  islp2 7697  cnsscnp 7722  opnin 7821  bcthlem21 7969  pilem2 8610  projlem28 9152  irredlem1 10254  mdsymlem4 10270  cdj3lem2b 10298  uninqs 10378  fiiu 10386  efilcp 10481  efilcp2 10486

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain