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  3557  po2nr  5451  wefrc  5513  tz7.7  6185  funssres  6368  isomin  7069  f1ocnv2d  7378  onint  7490  f1oweALT  7655  bropfvvvv  7770  wfrlem12  7949  tfrlem9  8004  tz7.49  8064  oelim  8142  oaordex  8167  omordi  8175  omass  8189  oen0  8195  nnmass  8233  nnmordi  8240  inf3lem2  9076  epfrs  9157  indcardi  9452  ackbij1lem16  9646  cfcoflem  9683  axcc3  9849  zorn2lem7  9913  grur1a  10230  genpcd  10417  genpnmax  10418  mulclprlem  10430  distrlem1pr  10436  ltaddpr  10445  ltexprlem6  10452  ltexprlem7  10453  mulgt0sr  10516  divgt0  11497  divge0  11498  sup2  11584  uzind2  12063  uzwo  12299  supxrun  12697  expnbnd  13589  facdiv  13643  hashimarni  13798  swrdswrdlem  14057  wrd2ind  14076  s3iunsndisj  14319  caubnd  14710  dvdsabseq  15655  lcmfunsnlem2lem1  15972  divgcdcoprm0  15999  ncoprmlnprm  16058  cshwshashlem1  16421  psgnunilem4  18617  lmodvsdi  19650  xrsdsreclblem  20137  cpmatacl  21321  riinopn  21513  0ntr  21676  elcls  21678  hausnei2  21958  fgfil  22480  alexsubALTlem2  22653  alexsubALT  22656  aalioulem3  24930  aalioulem4  24931  wilthlem3  25655  2sqreultlem  26031  2sqreunnltlem  26034  finsumvtxdg2size  27340  upgrewlkle2  27396  upgrwlkdvdelem  27525  uhgrwkspthlem2  27543  clwwlkinwwlk  27825  wwlksext2clwwlk  27842  1pthon2v  27938  n4cyclfrgr  28076  frgrnbnb  28078  frgrwopreglem4a  28095  frgrreg  28179  frgrregord013  28180  grpoidinvlem3  28289  elspansn5  29357  atcv1  30163  atcvatlem  30168  chirredlem3  30175  mdsymlem3  30188  mdsymlem5  30190  mdsymlem6  30191  sumdmdlem2  30202  f1o3d  30386  slmdvsdi  30893  satfv0fun  32731  satffunlem1lem1  32762  satffunlem2lem1  32764  fgmin  33831  nndivsub  33918  mblfinlem3  35096  rngonegrmul  35382  crngm23  35440  hlrelat2  36699  pmaple  37057  pmodlem2  37143  dalaw  37182  sn-sup2  39594  syl5imp  41218  com3rgbi  41220  ee223  41340  iccpartigtl  43940  iccelpart  43950  lighneallem3  44125  bgoldbtbndlem3  44325  isomgrsym  44354  isomgrtr  44357  nzerooringczr  44696  ply1mulgsumlem1  44794  fllog2  44982