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  1360  rspct  3562  po2nr  5546  wefrc  5618  tz7.7  6343  funssres  6536  isomin  7283  f1ocnv2d  7611  onint  7735  f1oweALT  7916  bropfvvvv  8034  tfrlem9  8316  tz7.49  8376  oelim  8461  oaordex  8485  omordi  8493  omass  8507  oen0  8514  nnmass  8552  nnmordi  8559  inf3lem2  9538  epfrs  9640  indcardi  9951  ackbij1lem16  10144  cfcoflem  10182  axcc3  10348  zorn2lem7  10412  grur1a  10730  genpcd  10917  genpnmax  10918  mulclprlem  10930  distrlem1pr  10936  ltaddpr  10945  ltexprlem6  10952  ltexprlem7  10953  mulgt0sr  11016  divgt0  12010  divge0  12011  sup2  12098  uzind2  12585  uzwo  12824  supxrun  13231  expnbnd  14155  facdiv  14210  hashimarni  14364  swrdswrdlem  14627  wrd2ind  14646  s3iunsndisj  14891  caubnd  15282  dvdsabseq  16240  lcmfunsnlem2lem1  16565  divgcdcoprm0  16592  ncoprmlnprm  16655  cshwshashlem1  17023  psgnunilem4  19426  lmodvsdi  20836  xrsdsreclblem  21367  nzerooringczr  21435  cpmatacl  22660  riinopn  22852  0ntr  23015  elcls  23017  hausnei2  23297  fgfil  23819  alexsubALTlem2  23992  alexsubALT  23995  aalioulem3  26298  aalioulem4  26299  wilthlem3  27036  2sqreultlem  27414  2sqreunnltlem  27417  bdayfinbndlem1  28463  finsumvtxdg2size  29624  upgrewlkle2  29680  upgrwlkdvdelem  29809  uhgrwkspthlem2  29827  clwwlkinwwlk  30115  wwlksext2clwwlk  30132  1pthon2v  30228  n4cyclfrgr  30366  frgrnbnb  30368  frgrwopreglem4a  30385  frgrreg  30469  frgrregord013  30470  grpoidinvlem3  30581  elspansn5  31649  atcv1  32455  atcvatlem  32460  chirredlem3  32467  mdsymlem3  32480  mdsymlem5  32482  mdsymlem6  32483  sumdmdlem2  32494  f1o3d  32704  slmdvsdi  33297  satfv0fun  35565  satffunlem1lem1  35596  satffunlem2lem1  35598  fgmin  36564  nndivsub  36651  mblfinlem3  37860  rngonegrmul  38145  crngm23  38203  hlrelat2  39663  pmaple  40021  pmodlem2  40107  dalaw  40146  sn-sup2  42746  syl5imp  44753  com3rgbi  44755  ee223  44875  relpmin  45193  2tceilhalfelfzo1  47578  iccpartigtl  47669  iccelpart  47679  lighneallem3  47853  bgoldbtbndlem3  48053  uhgrimisgrgric  48177  clnbgrgrim  48180  clnbgr3stgrgrlic  48266  gpgusgralem  48302  gpgvtxedg0  48309  gpgvtxedg1  48310  ply1mulgsumlem1  48632  fllog2  48814