Theorem com34 92

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 87. Double deduction associated with com12 33. (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 91	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 36	1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  93  com35  99  3an1rs  1378  rspct  3562  po2nr  5572  wefrc  5644  tz7.7  6388  funssres  6584  isomin  7345  f1ocnv2d  7674  onint  7804  f1oweALT  7984  bropfvvvv  8103  tfrlem9  8396  tz7.49  8458  oelim  8545  oaordex  8569  omordi  8577  omass  8591  oen0  8598  nnmass  8636  nnmordi  8643  inf3lem2  9633  epfrs  9735  indcardi  10123  ackbij1lem16  10315  cfcoflem  10353  axcc3  10519  zorn2lem7  10583  grur1a  10907  genpcd  11094  genpnmax  11095  mulclprlem  11107  distrlem1pr  11113  ltaddpr  11122  ltexprlem6  11129  ltexprlem7  11130  mulgt0sr  11193  divgt0  12188  divge0  12189  sup2  12276  uzind2  12795  uzwo  13041  supxrun  13449  expnbnd  14379  facdiv  14434  hashimarni  14589  swrdswrdlem  14857  wrd2ind  14876  s3iunsndisj  15126  caubnd  15531  dvdsabseq  16488  lcmfunsnlem2lem1  16818  divgcdcoprm0  16845  ncoprmlnprm  16909  cshwshashlem1  17278  psgnunilem4  19716  lmodvsdi  21165  xrsdsreclblem  21724  nzerooringczr  21791  cpmatacl  23039  riinopn  23231  0ntr  23394  elcls  23396  hausnei2  23676  fgfil  24199  alexsubALTlem2  24372  alexsubALT  24375  aalioulem3  26666  aalioulem4  26667  wilthlem3  27402  2sqreultlem  27779  2sqreunnltlem  27782  bdayfinbndlem1  28858  finsumvtxdg2size  30136  upgrewlkle2  30192  upgrwlkdvdelem  30327  uhgrwkspthlem2  30345  clwwlkinwwlk  30636  wwlksext2clwwlk  30653  1pthon2v  30759  n4cyclfrgr  30897  frgrnbnb  30899  frgrwopreglem4a  30916  frgrreg  31000  frgrregord013  31001  grpoidinvlem3  31113  elspansn5  32181  atcv1  32987  atcvatlem  32992  chirredlem3  32999  mdsymlem3  33012  mdsymlem5  33014  mdsymlem6  33015  sumdmdlem2  33026  f1o3d  33267  slmdvsdi  33822  satfv0fun  36222  satffunlem1lem1  36253  satffunlem2lem1  36255  fgmin  37250  nndivsub  37337  mblfinlem3  38670  rngonegrmul  38971  crngm23  39029  hlrelat2  40553  pmaple  40911  pmodlem2  40997  dalaw  41036  sn-sup2  43648  syl5imp  45588  com3rgbi  45590  ee223  45710  relpmin  46035  2tceilhalfelfzo1  48499  iccpartigtl  48598  iccelpart  48608  lighneallem3  48785  bgoldbtbndlem3  48998  uhgrimisgrgric  49122  clnbgrgrim  49125  clnbgr3stgrgrlic  49211  gpgusgralem  49247  gpgvtxedg0  49254  gpgvtxedg1  49255  ply1mulgsumlem1  49591  fllog2  49773