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  1279  ad5ant14  1302  ad5ant15  1303  ad5ant24  1305  ad5ant25  1306  ad5ant124  1311  ad5ant134  1313  ad5ant135  1314  rspct  3302  po2nr  5048  wefrc  5108  tz7.7  5749  funssres  5930  isomin  6587  f1ocnv2d  6886  onint  6995  f1oweALT  7152  bropfvvvv  7257  wfrlem12  7426  tfrlem9  7481  tz7.49  7540  oelim  7614  oaordex  7638  omordi  7646  omass  7660  oen0  7666  nnmass  7704  nnmordi  7711  inf3lem2  8526  epfrs  8607  indcardi  8864  ackbij1lem16  9057  cfcoflem  9094  axcc3  9260  zorn2lem7  9324  grur1a  9641  genpcd  9828  genpnmax  9829  mulclprlem  9841  distrlem1pr  9847  ltaddpr  9856  ltexprlem6  9863  ltexprlem7  9864  mulgt0sr  9926  divgt0  10891  divge0  10892  sup2  10979  uzind2  11470  uzwo  11751  supxrun  12146  expnbnd  12993  facdiv  13074  hashimarni  13228  swrdswrdlem  13459  wrd2ind  13477  s3iunsndisj  13707  caubnd  14098  dvdsabseq  15035  lcmfunsnlem2lem1  15351  divgcdcoprm0  15379  ncoprmlnprm  15436  cshwshashlem1  15802  psgnunilem4  17917  lmodvsdi  18886  xrsdsreclblem  19792  cpmatacl  20521  riinopn  20713  0ntr  20875  elcls  20877  hausnei2  21157  fgfil  21679  alexsubALTlem2  21852  alexsubALT  21855  aalioulem3  24089  aalioulem4  24090  wilthlem3  24796  finsumvtxdg2size  26446  upgrewlkle2  26502  upgrwlkdvdelem  26632  uhgrwkspthlem2  26650  clwwlkinwwlk  26905  1pthon2v  27013  n4cyclfrgr  27155  frgrnbnb  27157  frgrwopreglem4a  27174  frgrreg  27252  frgrregord013  27253  grpoidinvlem3  27360  elspansn5  28433  atcv1  29239  atcvatlem  29244  chirredlem3  29251  mdsymlem3  29264  mdsymlem5  29266  mdsymlem6  29267  sumdmdlem2  29278  f1o3d  29431  slmdvsdi  29768  frrlem11  31792  fgmin  32365  nndivsub  32456  mblfinlem3  33448  rngonegrmul  33743  crngm23  33801  hlrelat2  34689  pmaple  35047  pmodlem2  35133  dalaw  35172  syl5imp  38718  com3rgbi  38720  ee223  38859  iccpartigtl  41359  iccelpart  41369  lighneallem3  41524  bgoldbtbndlem3  41695  nzerooringczr  42072  ply1mulgsumlem1  42174  fllog2  42362