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  1359  rspct  3621  po2nr  5622  wefrc  5694  tz7.7  6421  funssres  6622  isomin  7373  f1ocnv2d  7703  onint  7826  f1oweALT  8013  bropfvvvv  8133  wfrlem12OLD  8376  tfrlem9  8441  tz7.49  8501  oelim  8590  oaordex  8614  omordi  8622  omass  8636  oen0  8642  nnmass  8680  nnmordi  8687  inf3lem2  9698  epfrs  9800  indcardi  10110  ackbij1lem16  10303  cfcoflem  10341  axcc3  10507  zorn2lem7  10571  grur1a  10888  genpcd  11075  genpnmax  11076  mulclprlem  11088  distrlem1pr  11094  ltaddpr  11103  ltexprlem6  11110  ltexprlem7  11111  mulgt0sr  11174  divgt0  12163  divge0  12164  sup2  12251  uzind2  12736  uzwo  12976  supxrun  13378  expnbnd  14281  facdiv  14336  hashimarni  14490  swrdswrdlem  14752  wrd2ind  14771  s3iunsndisj  15017  caubnd  15407  dvdsabseq  16361  lcmfunsnlem2lem1  16685  divgcdcoprm0  16712  ncoprmlnprm  16775  cshwshashlem1  17143  psgnunilem4  19539  lmodvsdi  20905  xrsdsreclblem  21453  nzerooringczr  21514  cpmatacl  22743  riinopn  22935  0ntr  23100  elcls  23102  hausnei2  23382  fgfil  23904  alexsubALTlem2  24077  alexsubALT  24080  aalioulem3  26394  aalioulem4  26395  wilthlem3  27131  2sqreultlem  27509  2sqreunnltlem  27512  finsumvtxdg2size  29586  upgrewlkle2  29642  upgrwlkdvdelem  29772  uhgrwkspthlem2  29790  clwwlkinwwlk  30072  wwlksext2clwwlk  30089  1pthon2v  30185  n4cyclfrgr  30323  frgrnbnb  30325  frgrwopreglem4a  30342  frgrreg  30426  frgrregord013  30427  grpoidinvlem3  30538  elspansn5  31606  atcv1  32412  atcvatlem  32417  chirredlem3  32424  mdsymlem3  32437  mdsymlem5  32439  mdsymlem6  32440  sumdmdlem2  32451  f1o3d  32646  slmdvsdi  33194  satfv0fun  35339  satffunlem1lem1  35370  satffunlem2lem1  35372  fgmin  36336  nndivsub  36423  mblfinlem3  37619  rngonegrmul  37904  crngm23  37962  hlrelat2  39360  pmaple  39718  pmodlem2  39804  dalaw  39843  sn-sup2  42447  syl5imp  44483  com3rgbi  44485  ee223  44605  iccpartigtl  47297  iccelpart  47307  lighneallem3  47481  bgoldbtbndlem3  47681  uhgrimisgrgric  47783  clnbgrgrim  47786  ply1mulgsumlem1  48115  fllog2  48302