Theorem com34 91

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 86. Double deduction associated with com12 32. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
com34	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

Proof of Theorem com34

Step	Hyp	Ref	Expression
1		com4.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2		pm2.04 90	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 35	1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

Syntax hints:   → wi 4

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

This theorem is referenced by:  com4l  92  com35  98  3an1rs  1356  rspct  3592  po2nr  5604  wefrc  5672  tz7.7  6397  funssres  6598  isomin  7344  f1ocnv2d  7674  onint  7794  f1oweALT  7977  bropfvvvv  8097  wfrlem12OLD  8341  tfrlem9  8406  tz7.49  8466  oelim  8555  oaordex  8579  omordi  8587  omass  8601  oen0  8607  nnmass  8645  nnmordi  8652  inf3lem2  9654  epfrs  9756  indcardi  10066  ackbij1lem16  10260  cfcoflem  10297  axcc3  10463  zorn2lem7  10527  grur1a  10844  genpcd  11031  genpnmax  11032  mulclprlem  11044  distrlem1pr  11050  ltaddpr  11059  ltexprlem6  11066  ltexprlem7  11067  mulgt0sr  11130  divgt0  12115  divge0  12116  sup2  12203  uzind2  12688  uzwo  12928  supxrun  13330  expnbnd  14230  facdiv  14282  hashimarni  14436  swrdswrdlem  14690  wrd2ind  14709  s3iunsndisj  14951  caubnd  15341  dvdsabseq  16293  lcmfunsnlem2lem1  16612  divgcdcoprm0  16639  ncoprmlnprm  16703  cshwshashlem1  17068  psgnunilem4  19464  lmodvsdi  20780  xrsdsreclblem  21362  nzerooringczr  21423  cpmatacl  22662  riinopn  22854  0ntr  23019  elcls  23021  hausnei2  23301  fgfil  23823  alexsubALTlem2  23996  alexsubALT  23999  aalioulem3  26314  aalioulem4  26315  wilthlem3  27047  2sqreultlem  27425  2sqreunnltlem  27428  finsumvtxdg2size  29436  upgrewlkle2  29492  upgrwlkdvdelem  29622  uhgrwkspthlem2  29640  clwwlkinwwlk  29922  wwlksext2clwwlk  29939  1pthon2v  30035  n4cyclfrgr  30173  frgrnbnb  30175  frgrwopreglem4a  30192  frgrreg  30276  frgrregord013  30277  grpoidinvlem3  30388  elspansn5  31456  atcv1  32262  atcvatlem  32267  chirredlem3  32274  mdsymlem3  32287  mdsymlem5  32289  mdsymlem6  32290  sumdmdlem2  32301  f1o3d  32493  slmdvsdi  33014  satfv0fun  35112  satffunlem1lem1  35143  satffunlem2lem1  35145  fgmin  35985  nndivsub  36072  mblfinlem3  37263  rngonegrmul  37548  crngm23  37606  hlrelat2  39006  pmaple  39364  pmodlem2  39450  dalaw  39489  sn-sup2  42159  syl5imp  44093  com3rgbi  44095  ee223  44215  iccpartigtl  46900  iccelpart  46910  lighneallem3  47084  bgoldbtbndlem3  47284  ply1mulgsumlem1  47640  fllog2  47827