Theorem com34 89

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 84. (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 88	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 34	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  90  com35  96  3an1rs  1271  ad5ant14  1294  ad5ant15  1295  ad5ant24  1297  ad5ant25  1298  ad5ant124  1303  ad5ant134  1305  ad5ant135  1306  rspct  3275  po2nr  4972  wefrc  5032  tz7.7  5666  funssres  5844  isomin  6487  f1ocnv2d  6784  onint  6887  f1oweALT  7043  bropfvvvv  7144  wfrlem12  7313  tfrlem9  7368  tz7.49  7427  oelim  7501  oaordex  7525  omordi  7533  omass  7547  oen0  7553  nnmass  7591  nnmordi  7598  inf3lem2  8409  epfrs  8490  indcardi  8747  ackbij1lem16  8940  cfcoflem  8977  axcc3  9143  zorn2lem7  9207  grur1a  9520  genpcd  9707  genpnmax  9708  mulclprlem  9720  distrlem1pr  9726  ltaddpr  9735  ltexprlem6  9742  ltexprlem7  9743  mulgt0sr  9805  divgt0  10770  divge0  10771  sup2  10858  uzind2  11346  uzwo  11627  supxrun  12018  expnbnd  12855  facdiv  12936  hashimarni  13086  swrdswrdlem  13311  wrd2ind  13329  s3iunsndisj  13555  caubnd  13946  dvdsabseq  14873  lcmfunsnlem2lem1  15189  divgcdcoprm0  15217  ncoprmlnprm  15274  cshwshashlem1  15640  psgnunilem4  17740  lmodvsdi  18709  xrsdsreclblem  19611  cpmatacl  20340  riinopn  20538  0ntr  20685  elcls  20687  hausnei2  20967  fgfil  21489  alexsubALTlem2  21662  alexsubALT  21665  aalioulem3  23893  aalioulem4  23894  wilthlem3  24596  usgra2adedgspthlem2  26140  nbhashuvtx1  26442  3cyclfrgrarn  26540  n4cyclfrgra  26545  frgraregord013  26645  grpoidinvlem3  26744  elspansn5  27817  atcv1  28623  atcvatlem  28628  chirredlem3  28635  mdsymlem3  28648  mdsymlem5  28650  mdsymlem6  28651  sumdmdlem2  28662  f1o3d  28813  slmdvsdi  29099  frrlem11  31036  fgmin  31535  nndivsub  31626  mblfinlem3  32618  rngonegrmul  32913  crngm23  32971  hlrelat2  33707  pmaple  34065  pmodlem2  34151  dalaw  34190  syl5imp  37739  com3rgbi  37741  ee223  37880  iccpartigtl  39961  iccelpart  39971  lighneallem3  40062  bgoldbtbndlem3  40223  upgrewlkle2  40808  upgrwlkdvdelem  40942  uhgr1wlkspthlem2  40960  cyclnsPth  41006  1wlkiswwlks1  41064  1pthon2v-av  41320  n4cyclfrgr  41461  frgrnbnb  41463  av-frgrareg  41548  av-frgraregord013  41549  nzerooringczr  41864  ply1mulgsumlem1  41968  fllog2  42160