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  1366  rspct  3553  po2nr  5547  wefrc  5619  tz7.7  6343  funssres  6536  isomin  7288  f1ocnv2d  7616  onint  7740  f1oweALT  7921  bropfvvvv  8038  tfrlem9  8321  tz7.49  8381  oelim  8466  oaordex  8490  omordi  8498  omass  8512  oen0  8519  nnmass  8557  nnmordi  8564  inf3lem2  9548  epfrs  9650  indcardi  9961  ackbij1lem16  10154  cfcoflem  10192  axcc3  10358  zorn2lem7  10422  grur1a  10740  genpcd  10927  genpnmax  10928  mulclprlem  10940  distrlem1pr  10946  ltaddpr  10955  ltexprlem6  10962  ltexprlem7  10963  mulgt0sr  11026  divgt0  12022  divge0  12023  sup2  12110  uzind2  12620  uzwo  12859  supxrun  13266  expnbnd  14192  facdiv  14247  hashimarni  14401  swrdswrdlem  14664  wrd2ind  14683  s3iunsndisj  14928  caubnd  15319  dvdsabseq  16280  lcmfunsnlem2lem1  16605  divgcdcoprm0  16632  ncoprmlnprm  16696  cshwshashlem1  17064  psgnunilem4  19470  lmodvsdi  20882  xrsdsreclblem  21395  nzerooringczr  21462  cpmatacl  22706  riinopn  22898  0ntr  23061  elcls  23063  hausnei2  23343  fgfil  23865  alexsubALTlem2  24038  alexsubALT  24041  aalioulem3  26325  aalioulem4  26326  wilthlem3  27058  2sqreultlem  27435  2sqreunnltlem  27438  bdayfinbndlem1  28484  finsumvtxdg2size  29644  upgrewlkle2  29700  upgrwlkdvdelem  29829  uhgrwkspthlem2  29847  clwwlkinwwlk  30135  wwlksext2clwwlk  30152  1pthon2v  30248  n4cyclfrgr  30386  frgrnbnb  30388  frgrwopreglem4a  30405  frgrreg  30489  frgrregord013  30490  grpoidinvlem3  30602  elspansn5  31670  atcv1  32476  atcvatlem  32481  chirredlem3  32488  mdsymlem3  32501  mdsymlem5  32503  mdsymlem6  32504  sumdmdlem2  32515  f1o3d  32725  slmdvsdi  33303  satfv0fun  35606  satffunlem1lem1  35637  satffunlem2lem1  35639  fgmin  36605  nndivsub  36692  mblfinlem3  38033  rngonegrmul  38318  crngm23  38376  hlrelat2  39902  pmaple  40260  pmodlem2  40346  dalaw  40385  sn-sup2  42988  syl5imp  44963  com3rgbi  44965  ee223  45085  relpmin  45403  2tceilhalfelfzo1  47806  iccpartigtl  47905  iccelpart  47915  lighneallem3  48092  bgoldbtbndlem3  48305  uhgrimisgrgric  48429  clnbgrgrim  48432  clnbgr3stgrgrlic  48518  gpgusgralem  48554  gpgvtxedg0  48561  gpgvtxedg1  48562  ply1mulgsumlem1  48884  fllog2  49066