Theorem com34 36

Description: Commutation of antecedents. Swap 3rd and 4th.

Hypothesis

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

Assertion

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

Proof of Theorem com34

Step	Hyp	Ref	Expression
1		com4.1	. 2 |- (ph -> (ps -> (ch -> (th -> ta ))))
2		pm2.04 31	. 2 |- ((ch -> (th -> ta )) -> (th -> (ch -> ta )))
3	1, 2	syl6 23	1 |- (ph -> (ps -> (th -> (ch -> ta ))))

Syntax hints:   -> wi 2

This theorem is referenced by:  com24 37  com14 38  po2nr 2135  wefrc 2195  tz7.7 2224  onint 2261  limsuc 2361  funssres 2698  isomin 2937  f1oweOLD 2944  tfrlem9 2957  tz7.49 2997  oelim 3137  oaordex 3160  omordi 3164  oen0 3165  nnmass 3181  nnmordi 3188  en3d 3304  inf3lem2 3465  zfregs 3491  zornlem7 3609  genpcd 3903  genpnmax 3904  mulclprlem 3915  ltaddpr 3934  ltexprlem6 3941  ltexprlem7 3942  prlem936b 3948  sup2 4510  uzwo 4605  nnwoOLD 4608  uzwo3lem1 4614  qbtwnre 4650  infxpidmlem11 4943  elspansn5t 5479  atcv1 5768  atcvatlem 5770  mdsymlem3 5778  mdsymlem5 5780  mdsymlem6 5781  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org