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  5541  wefrc  5613  tz7.7  6333  funssres  6526  isomin  7274  f1ocnv2d  7602  onint  7726  f1oweALT  7907  bropfvvvv  8025  tfrlem9  8307  tz7.49  8367  oelim  8452  oaordex  8476  omordi  8484  omass  8498  oen0  8504  nnmass  8542  nnmordi  8549  inf3lem2  9525  epfrs  9627  indcardi  9935  ackbij1lem16  10128  cfcoflem  10166  axcc3  10332  zorn2lem7  10396  grur1a  10713  genpcd  10900  genpnmax  10901  mulclprlem  10913  distrlem1pr  10919  ltaddpr  10928  ltexprlem6  10935  ltexprlem7  10936  mulgt0sr  10999  divgt0  11993  divge0  11994  sup2  12081  uzind2  12569  uzwo  12812  supxrun  13218  expnbnd  14139  facdiv  14194  hashimarni  14348  swrdswrdlem  14610  wrd2ind  14629  s3iunsndisj  14875  caubnd  15266  dvdsabseq  16224  lcmfunsnlem2lem1  16549  divgcdcoprm0  16576  ncoprmlnprm  16639  cshwshashlem1  17007  psgnunilem4  19376  lmodvsdi  20788  xrsdsreclblem  21319  nzerooringczr  21387  cpmatacl  22601  riinopn  22793  0ntr  22956  elcls  22958  hausnei2  23238  fgfil  23760  alexsubALTlem2  23933  alexsubALT  23936  aalioulem3  26240  aalioulem4  26241  wilthlem3  26978  2sqreultlem  27356  2sqreunnltlem  27359  finsumvtxdg2size  29496  upgrewlkle2  29552  upgrwlkdvdelem  29681  uhgrwkspthlem2  29699  clwwlkinwwlk  29984  wwlksext2clwwlk  30001  1pthon2v  30097  n4cyclfrgr  30235  frgrnbnb  30237  frgrwopreglem4a  30254  frgrreg  30338  frgrregord013  30339  grpoidinvlem3  30450  elspansn5  31518  atcv1  32324  atcvatlem  32329  chirredlem3  32336  mdsymlem3  32349  mdsymlem5  32351  mdsymlem6  32352  sumdmdlem2  32363  f1o3d  32569  slmdvsdi  33157  satfv0fun  35344  satffunlem1lem1  35375  satffunlem2lem1  35377  fgmin  36344  nndivsub  36431  mblfinlem3  37639  rngonegrmul  37924  crngm23  37982  hlrelat2  39382  pmaple  39740  pmodlem2  39826  dalaw  39865  sn-sup2  42464  syl5imp  44486  com3rgbi  44488  ee223  44608  relpmin  44926  2tceilhalfelfzo1  47316  iccpartigtl  47407  iccelpart  47417  lighneallem3  47591  bgoldbtbndlem3  47791  uhgrimisgrgric  47915  clnbgrgrim  47918  clnbgr3stgrgrlic  48004  gpgusgralem  48040  gpgvtxedg0  48047  gpgvtxedg1  48048  ply1mulgsumlem1  48371  fllog2  48553