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  3563  po2nr  5538  wefrc  5610  tz7.7  6332  funssres  6525  isomin  7271  f1ocnv2d  7599  onint  7723  f1oweALT  7904  bropfvvvv  8022  tfrlem9  8304  tz7.49  8364  oelim  8449  oaordex  8473  omordi  8481  omass  8495  oen0  8501  nnmass  8539  nnmordi  8546  inf3lem2  9519  epfrs  9621  indcardi  9932  ackbij1lem16  10125  cfcoflem  10163  axcc3  10329  zorn2lem7  10393  grur1a  10710  genpcd  10897  genpnmax  10898  mulclprlem  10910  distrlem1pr  10916  ltaddpr  10925  ltexprlem6  10932  ltexprlem7  10933  mulgt0sr  10996  divgt0  11990  divge0  11991  sup2  12078  uzind2  12566  uzwo  12809  supxrun  13215  expnbnd  14139  facdiv  14194  hashimarni  14348  swrdswrdlem  14611  wrd2ind  14630  s3iunsndisj  14875  caubnd  15266  dvdsabseq  16224  lcmfunsnlem2lem1  16549  divgcdcoprm0  16576  ncoprmlnprm  16639  cshwshashlem1  17007  psgnunilem4  19410  lmodvsdi  20819  xrsdsreclblem  21350  nzerooringczr  21418  cpmatacl  22632  riinopn  22824  0ntr  22987  elcls  22989  hausnei2  23269  fgfil  23791  alexsubALTlem2  23964  alexsubALT  23967  aalioulem3  26270  aalioulem4  26271  wilthlem3  27008  2sqreultlem  27386  2sqreunnltlem  27389  finsumvtxdg2size  29530  upgrewlkle2  29586  upgrwlkdvdelem  29715  uhgrwkspthlem2  29733  clwwlkinwwlk  30018  wwlksext2clwwlk  30035  1pthon2v  30131  n4cyclfrgr  30269  frgrnbnb  30271  frgrwopreglem4a  30288  frgrreg  30372  frgrregord013  30373  grpoidinvlem3  30484  elspansn5  31552  atcv1  32358  atcvatlem  32363  chirredlem3  32370  mdsymlem3  32383  mdsymlem5  32385  mdsymlem6  32386  sumdmdlem2  32397  f1o3d  32606  slmdvsdi  33182  satfv0fun  35413  satffunlem1lem1  35444  satffunlem2lem1  35446  fgmin  36410  nndivsub  36497  mblfinlem3  37705  rngonegrmul  37990  crngm23  38048  hlrelat2  39448  pmaple  39806  pmodlem2  39892  dalaw  39931  sn-sup2  42530  syl5imp  44551  com3rgbi  44553  ee223  44673  relpmin  44991  2tceilhalfelfzo1  47369  iccpartigtl  47460  iccelpart  47470  lighneallem3  47644  bgoldbtbndlem3  47844  uhgrimisgrgric  47968  clnbgrgrim  47971  clnbgr3stgrgrlic  48057  gpgusgralem  48093  gpgvtxedg0  48100  gpgvtxedg1  48101  ply1mulgsumlem1  48424  fllog2  48606