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  1361  rspct  3550  po2nr  5553  wefrc  5625  tz7.7  6349  funssres  6542  isomin  7292  f1ocnv2d  7620  onint  7744  f1oweALT  7925  bropfvvvv  8042  tfrlem9  8324  tz7.49  8384  oelim  8469  oaordex  8493  omordi  8501  omass  8515  oen0  8522  nnmass  8560  nnmordi  8567  inf3lem2  9550  epfrs  9652  indcardi  9963  ackbij1lem16  10156  cfcoflem  10194  axcc3  10360  zorn2lem7  10424  grur1a  10742  genpcd  10929  genpnmax  10930  mulclprlem  10942  distrlem1pr  10948  ltaddpr  10957  ltexprlem6  10964  ltexprlem7  10965  mulgt0sr  11028  divgt0  12024  divge0  12025  sup2  12112  uzind2  12622  uzwo  12861  supxrun  13268  expnbnd  14194  facdiv  14249  hashimarni  14403  swrdswrdlem  14666  wrd2ind  14685  s3iunsndisj  14930  caubnd  15321  dvdsabseq  16282  lcmfunsnlem2lem1  16607  divgcdcoprm0  16634  ncoprmlnprm  16698  cshwshashlem1  17066  psgnunilem4  19472  lmodvsdi  20880  xrsdsreclblem  21393  nzerooringczr  21460  cpmatacl  22681  riinopn  22873  0ntr  23036  elcls  23038  hausnei2  23318  fgfil  23840  alexsubALTlem2  24013  alexsubALT  24016  aalioulem3  26300  aalioulem4  26301  wilthlem3  27033  2sqreultlem  27410  2sqreunnltlem  27413  bdayfinbndlem1  28459  finsumvtxdg2size  29619  upgrewlkle2  29675  upgrwlkdvdelem  29804  uhgrwkspthlem2  29822  clwwlkinwwlk  30110  wwlksext2clwwlk  30127  1pthon2v  30223  n4cyclfrgr  30361  frgrnbnb  30363  frgrwopreglem4a  30380  frgrreg  30464  frgrregord013  30465  grpoidinvlem3  30577  elspansn5  31645  atcv1  32451  atcvatlem  32456  chirredlem3  32463  mdsymlem3  32476  mdsymlem5  32478  mdsymlem6  32479  sumdmdlem2  32490  f1o3d  32699  slmdvsdi  33276  satfv0fun  35553  satffunlem1lem1  35584  satffunlem2lem1  35586  fgmin  36552  nndivsub  36639  mblfinlem3  37980  rngonegrmul  38265  crngm23  38323  hlrelat2  39849  pmaple  40207  pmodlem2  40293  dalaw  40332  sn-sup2  42936  syl5imp  44939  com3rgbi  44941  ee223  45061  relpmin  45379  2tceilhalfelfzo1  47784  iccpartigtl  47883  iccelpart  47893  lighneallem3  48070  bgoldbtbndlem3  48283  uhgrimisgrgric  48407  clnbgrgrim  48410  clnbgr3stgrgrlic  48496  gpgusgralem  48532  gpgvtxedg0  48539  gpgvtxedg1  48540  ply1mulgsumlem1  48862  fllog2  49044