Theorem com34 92

Description: Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23 87. Double deduction associated with com12 33. (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 91	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 36	1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  93  com35  99  3an1rs  1378  rspct  3565  po2nr  5581  wefrc  5653  tz7.7  6387  funssres  6581  isomin  7342  f1ocnv2d  7671  onint  7793  f1oweALT  7973  bropfvvvv  8093  tfrlem9  8378  tz7.49  8438  oelim  8525  oaordex  8549  omordi  8557  omass  8571  oen0  8578  nnmass  8616  nnmordi  8623  inf3lem2  9612  epfrs  9714  indcardi  10048  ackbij1lem16  10240  cfcoflem  10278  axcc3  10444  zorn2lem7  10508  grur1a  10832  genpcd  11019  genpnmax  11020  mulclprlem  11032  distrlem1pr  11038  ltaddpr  11047  ltexprlem6  11054  ltexprlem7  11055  mulgt0sr  11118  divgt0  12111  divge0  12112  sup2  12199  uzind2  12718  uzwo  12964  supxrun  13372  expnbnd  14300  facdiv  14355  hashimarni  14510  swrdswrdlem  14777  wrd2ind  14796  s3iunsndisj  15045  caubnd  15450  dvdsabseq  16409  lcmfunsnlem2lem1  16734  divgcdcoprm0  16761  ncoprmlnprm  16825  cshwshashlem1  17193  psgnunilem4  19630  lmodvsdi  21075  xrsdsreclblem  21632  nzerooringczr  21699  cpmatacl  22947  riinopn  23139  0ntr  23302  elcls  23304  hausnei2  23584  fgfil  24107  alexsubALTlem2  24280  alexsubALT  24283  aalioulem3  26577  aalioulem4  26578  wilthlem3  27314  2sqreultlem  27691  2sqreunnltlem  27694  bdayfinbndlem1  28740  finsumvtxdg2size  30018  upgrewlkle2  30074  upgrwlkdvdelem  30209  uhgrwkspthlem2  30227  clwwlkinwwlk  30518  wwlksext2clwwlk  30535  1pthon2v  30641  n4cyclfrgr  30779  frgrnbnb  30781  frgrwopreglem4a  30798  frgrreg  30882  frgrregord013  30883  grpoidinvlem3  30995  elspansn5  32063  atcv1  32869  atcvatlem  32874  chirredlem3  32881  mdsymlem3  32894  mdsymlem5  32896  mdsymlem6  32897  sumdmdlem2  32908  f1o3d  33107  slmdvsdi  33663  satfv0fun  35958  satffunlem1lem1  35989  satffunlem2lem1  35991  fgmin  36997  nndivsub  37084  mblfinlem3  38416  rngonegrmul  38702  crngm23  38760  hlrelat2  40284  pmaple  40642  pmodlem2  40728  dalaw  40767  sn-sup2  43387  syl5imp  45343  com3rgbi  45345  ee223  45465  relpmin  45783  2tceilhalfelfzo1  48232  iccpartigtl  48331  iccelpart  48341  lighneallem3  48518  bgoldbtbndlem3  48731  uhgrimisgrgric  48855  clnbgrgrim  48858  clnbgr3stgrgrlic  48944  gpgusgralem  48980  gpgvtxedg0  48987  gpgvtxedg1  48988  ply1mulgsumlem1  49324  fllog2  49506