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  1360  rspct  3565  po2nr  5545  wefrc  5617  tz7.7  6337  funssres  6530  isomin  7278  f1ocnv2d  7606  onint  7730  f1oweALT  7914  bropfvvvv  8032  tfrlem9  8314  tz7.49  8374  oelim  8459  oaordex  8483  omordi  8491  omass  8505  oen0  8511  nnmass  8549  nnmordi  8556  inf3lem2  9544  epfrs  9646  indcardi  9954  ackbij1lem16  10147  cfcoflem  10185  axcc3  10351  zorn2lem7  10415  grur1a  10732  genpcd  10919  genpnmax  10920  mulclprlem  10932  distrlem1pr  10938  ltaddpr  10947  ltexprlem6  10954  ltexprlem7  10955  mulgt0sr  11018  divgt0  12011  divge0  12012  sup2  12099  uzind2  12587  uzwo  12830  supxrun  13236  expnbnd  14157  facdiv  14212  hashimarni  14366  swrdswrdlem  14628  wrd2ind  14647  s3iunsndisj  14893  caubnd  15284  dvdsabseq  16242  lcmfunsnlem2lem1  16567  divgcdcoprm0  16594  ncoprmlnprm  16657  cshwshashlem1  17025  psgnunilem4  19394  lmodvsdi  20806  xrsdsreclblem  21337  nzerooringczr  21405  cpmatacl  22619  riinopn  22811  0ntr  22974  elcls  22976  hausnei2  23256  fgfil  23778  alexsubALTlem2  23951  alexsubALT  23954  aalioulem3  26258  aalioulem4  26259  wilthlem3  26996  2sqreultlem  27374  2sqreunnltlem  27377  finsumvtxdg2size  29514  upgrewlkle2  29570  upgrwlkdvdelem  29699  uhgrwkspthlem2  29717  clwwlkinwwlk  30002  wwlksext2clwwlk  30019  1pthon2v  30115  n4cyclfrgr  30253  frgrnbnb  30255  frgrwopreglem4a  30272  frgrreg  30356  frgrregord013  30357  grpoidinvlem3  30468  elspansn5  31536  atcv1  32342  atcvatlem  32347  chirredlem3  32354  mdsymlem3  32367  mdsymlem5  32369  mdsymlem6  32370  sumdmdlem2  32381  f1o3d  32584  slmdvsdi  33170  satfv0fun  35346  satffunlem1lem1  35377  satffunlem2lem1  35379  fgmin  36346  nndivsub  36433  mblfinlem3  37641  rngonegrmul  37926  crngm23  37984  hlrelat2  39385  pmaple  39743  pmodlem2  39829  dalaw  39868  sn-sup2  42467  syl5imp  44489  com3rgbi  44491  ee223  44611  relpmin  44929  2tceilhalfelfzo1  47320  iccpartigtl  47411  iccelpart  47421  lighneallem3  47595  bgoldbtbndlem3  47795  uhgrimisgrgric  47919  clnbgrgrim  47922  clnbgr3stgrgrlic  48008  gpgusgralem  48044  gpgvtxedg0  48051  gpgvtxedg1  48052  ply1mulgsumlem1  48375  fllog2  48557