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  1357  rspct  3599  po2nr  5603  wefrc  5671  tz7.7  6391  funssres  6593  isomin  7338  f1ocnv2d  7663  onint  7782  f1oweALT  7963  bropfvvvv  8082  wfrlem12OLD  8324  tfrlem9  8389  tz7.49  8449  oelim  8538  oaordex  8562  omordi  8570  omass  8584  oen0  8590  nnmass  8628  nnmordi  8635  inf3lem2  9628  epfrs  9730  indcardi  10040  ackbij1lem16  10234  cfcoflem  10271  axcc3  10437  zorn2lem7  10501  grur1a  10818  genpcd  11005  genpnmax  11006  mulclprlem  11018  distrlem1pr  11024  ltaddpr  11033  ltexprlem6  11040  ltexprlem7  11041  mulgt0sr  11104  divgt0  12088  divge0  12089  sup2  12176  uzind2  12661  uzwo  12901  supxrun  13301  expnbnd  14201  facdiv  14253  hashimarni  14407  swrdswrdlem  14660  wrd2ind  14679  s3iunsndisj  14921  caubnd  15311  dvdsabseq  16262  lcmfunsnlem2lem1  16581  divgcdcoprm0  16608  ncoprmlnprm  16670  cshwshashlem1  17035  psgnunilem4  19408  lmodvsdi  20641  xrsdsreclblem  21193  cpmatacl  22440  riinopn  22632  0ntr  22797  elcls  22799  hausnei2  23079  fgfil  23601  alexsubALTlem2  23774  alexsubALT  23777  aalioulem3  26081  aalioulem4  26082  wilthlem3  26808  2sqreultlem  27184  2sqreunnltlem  27187  finsumvtxdg2size  29072  upgrewlkle2  29128  upgrwlkdvdelem  29258  uhgrwkspthlem2  29276  clwwlkinwwlk  29558  wwlksext2clwwlk  29575  1pthon2v  29671  n4cyclfrgr  29809  frgrnbnb  29811  frgrwopreglem4a  29828  frgrreg  29912  frgrregord013  29913  grpoidinvlem3  30024  elspansn5  31092  atcv1  31898  atcvatlem  31903  chirredlem3  31910  mdsymlem3  31923  mdsymlem5  31925  mdsymlem6  31926  sumdmdlem2  31937  f1o3d  32116  slmdvsdi  32628  satfv0fun  34658  satffunlem1lem1  34689  satffunlem2lem1  34691  fgmin  35560  nndivsub  35647  mblfinlem3  36832  rngonegrmul  37117  crngm23  37175  hlrelat2  38579  pmaple  38937  pmodlem2  39023  dalaw  39062  sn-sup2  41646  syl5imp  43577  com3rgbi  43579  ee223  43699  iccpartigtl  46391  iccelpart  46401  lighneallem3  46575  bgoldbtbndlem3  46775  isomgrsym  46804  isomgrtr  46807  nzerooringczr  47060  ply1mulgsumlem1  47156  fllog2  47343