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  1421  ad5ant124OLD  1429  ad5ant134OLD  1433  ad5ant135OLD  1435  rspct  3504  po2nr  5287  wefrc  5349  tz7.7  6002  funssres  6178  isomin  6859  f1ocnv2d  7163  onint  7273  f1oweALT  7429  bropfvvvv  7538  wfrlem12  7709  tfrlem9  7764  tz7.49  7823  oelim  7898  oaordex  7922  omordi  7930  omass  7944  oen0  7950  nnmass  7988  nnmordi  7995  inf3lem2  8823  epfrs  8904  indcardi  9197  ackbij1lem16  9392  cfcoflem  9429  axcc3  9595  zorn2lem7  9659  grur1a  9976  genpcd  10163  genpnmax  10164  mulclprlem  10176  distrlem1pr  10182  ltaddpr  10191  ltexprlem6  10198  ltexprlem7  10199  mulgt0sr  10262  divgt0  11245  divge0  11246  sup2  11333  uzind2  11822  uzwo  12058  supxrun  12458  expnbnd  13312  facdiv  13392  hashimarni  13542  swrdswrdlem  13813  wrd2ind  13844  wrd2indOLD  13845  s3iunsndisj  14116  caubnd  14505  dvdsabseq  15442  lcmfunsnlem2lem1  15757  divgcdcoprm0  15784  ncoprmlnprm  15840  cshwshashlem1  16201  psgnunilem4  18301  lmodvsdi  19278  xrsdsreclblem  20188  cpmatacl  20928  riinopn  21120  0ntr  21283  elcls  21285  hausnei2  21565  fgfil  22087  alexsubALTlem2  22260  alexsubALT  22263  aalioulem3  24526  aalioulem4  24527  wilthlem3  25248  finsumvtxdg2size  26898  upgrewlkle2  26954  upgrwlkdvdelem  27088  uhgrwkspthlem2  27106  clwwlkinwwlk  27429  clwwlkinwwlkOLD  27430  wwlksext2clwwlk  27454  1pthon2v  27556  n4cyclfrgr  27699  frgrnbnb  27701  frgrwopreglem4a  27718  frgrreg  27826  frgrregord013  27827  grpoidinvlem3  27933  elspansn5  29005  atcv1  29811  atcvatlem  29816  chirredlem3  29823  mdsymlem3  29836  mdsymlem5  29838  mdsymlem6  29839  sumdmdlem2  29850  f1o3d  29996  slmdvsdi  30330  fgmin  32953  nndivsub  33039  mblfinlem3  34074  rngonegrmul  34367  crngm23  34425  hlrelat2  35557  pmaple  35915  pmodlem2  36001  dalaw  36040  syl5imp  39672  com3rgbi  39674  ee223  39803  iccpartigtl  42391  iccelpart  42401  lighneallem3  42545  bgoldbtbndlem3  42720  isomgrsym  42749  isomgrtr  42752  nzerooringczr  43087  ply1mulgsumlem1  43189  fllog2  43377