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 1433  tfindsg 3162  isofrlem 3901  tfr3 3926  pssnn 4534  aceq5 4740  ltexprlem7 5148  bccl2t 6971  clm4le 7081  caucvglem4 7160  infxpidmlem11 7562  retopbas 7655  islp2 7747  cnsscnp 7772  opnin 7869  bcthlem21 8019  pilem2 8672  projlem28 9213  irredlem1 10317  mdsymlem4 10333  cdj3lem2b 10364  uninqs 10441  fiiu 10453  fiiuOLD 10454  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582

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

Copyright terms: Public domain