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  3587  po2nr  5575  wefrc  5648  tz7.7  6378  funssres  6580  isomin  7330  f1ocnv2d  7660  onint  7784  f1oweALT  7971  bropfvvvv  8091  wfrlem12OLD  8334  tfrlem9  8399  tz7.49  8459  oelim  8546  oaordex  8570  omordi  8578  omass  8592  oen0  8598  nnmass  8636  nnmordi  8643  inf3lem2  9643  epfrs  9745  indcardi  10055  ackbij1lem16  10248  cfcoflem  10286  axcc3  10452  zorn2lem7  10516  grur1a  10833  genpcd  11020  genpnmax  11021  mulclprlem  11033  distrlem1pr  11039  ltaddpr  11048  ltexprlem6  11055  ltexprlem7  11056  mulgt0sr  11119  divgt0  12110  divge0  12111  sup2  12198  uzind2  12686  uzwo  12927  supxrun  13332  expnbnd  14250  facdiv  14305  hashimarni  14459  swrdswrdlem  14722  wrd2ind  14741  s3iunsndisj  14987  caubnd  15377  dvdsabseq  16332  lcmfunsnlem2lem1  16657  divgcdcoprm0  16684  ncoprmlnprm  16747  cshwshashlem1  17115  psgnunilem4  19478  lmodvsdi  20842  xrsdsreclblem  21380  nzerooringczr  21441  cpmatacl  22654  riinopn  22846  0ntr  23009  elcls  23011  hausnei2  23291  fgfil  23813  alexsubALTlem2  23986  alexsubALT  23989  aalioulem3  26294  aalioulem4  26295  wilthlem3  27032  2sqreultlem  27410  2sqreunnltlem  27413  finsumvtxdg2size  29530  upgrewlkle2  29586  upgrwlkdvdelem  29718  uhgrwkspthlem2  29736  clwwlkinwwlk  30021  wwlksext2clwwlk  30038  1pthon2v  30134  n4cyclfrgr  30272  frgrnbnb  30274  frgrwopreglem4a  30291  frgrreg  30375  frgrregord013  30376  grpoidinvlem3  30487  elspansn5  31555  atcv1  32361  atcvatlem  32366  chirredlem3  32373  mdsymlem3  32386  mdsymlem5  32388  mdsymlem6  32389  sumdmdlem2  32400  f1o3d  32605  slmdvsdi  33212  satfv0fun  35393  satffunlem1lem1  35424  satffunlem2lem1  35426  fgmin  36388  nndivsub  36475  mblfinlem3  37683  rngonegrmul  37968  crngm23  38026  hlrelat2  39422  pmaple  39780  pmodlem2  39866  dalaw  39905  sn-sup2  42514  syl5imp  44537  com3rgbi  44539  ee223  44659  relpmin  44977  2tceilhalfelfzo1  47361  iccpartigtl  47437  iccelpart  47447  lighneallem3  47621  bgoldbtbndlem3  47821  uhgrimisgrgric  47944  clnbgrgrim  47947  clnbgr3stgrgrlic  48024  gpgusgralem  48060  gpgvtxedg0  48067  gpgvtxedg1  48068  ply1mulgsumlem1  48362  fllog2  48548