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  3566  po2nr  5578  wefrc  5650  tz7.7  6409  funssres  6607  isomin  7371  f1ocnv2d  7701  onint  7831  f1oweALT  8011  bropfvvvv  8131  tfrlem9  8424  tz7.49  8486  oelim  8573  oaordex  8597  omordi  8605  omass  8619  oen0  8626  nnmass  8664  nnmordi  8671  inf3lem2  9660  epfrs  9762  indcardi  10150  ackbij1lem16  10342  cfcoflem  10380  axcc3  10546  zorn2lem7  10610  grur1a  10934  genpcd  11121  genpnmax  11122  mulclprlem  11134  distrlem1pr  11140  ltaddpr  11149  ltexprlem6  11156  ltexprlem7  11157  mulgt0sr  11220  divgt0  12215  divge0  12216  sup2  12303  uzind2  12822  uzwo  13068  supxrun  13476  expnbnd  14406  facdiv  14461  hashimarni  14616  swrdswrdlem  14884  wrd2ind  14903  s3iunsndisj  15153  caubnd  15558  dvdsabseq  16515  lcmfunsnlem2lem1  16845  divgcdcoprm0  16872  ncoprmlnprm  16936  cshwshashlem1  17305  psgnunilem4  19744  lmodvsdi  21193  xrsdsreclblem  21752  nzerooringczr  21819  cpmatacl  23067  riinopn  23259  0ntr  23422  elcls  23424  hausnei2  23704  fgfil  24227  alexsubALTlem2  24400  alexsubALT  24403  aalioulem3  26694  aalioulem4  26695  wilthlem3  27430  2sqreultlem  27807  2sqreunnltlem  27810  bdayfinbndlem1  28886  finsumvtxdg2size  30164  upgrewlkle2  30220  upgrwlkdvdelem  30355  uhgrwkspthlem2  30373  clwwlkinwwlk  30664  wwlksext2clwwlk  30681  1pthon2v  30787  n4cyclfrgr  30925  frgrnbnb  30927  frgrwopreglem4a  30944  frgrreg  31028  frgrregord013  31029  grpoidinvlem3  31141  elspansn5  32209  atcv1  33015  atcvatlem  33020  chirredlem3  33027  mdsymlem3  33040  mdsymlem5  33042  mdsymlem6  33043  sumdmdlem2  33054  f1o3d  33295  slmdvsdi  33852  satfv0fun  36316  satffunlem1lem1  36347  satffunlem2lem1  36349  fgmin  37349  nndivsub  37436  mblfinlem3  38782  rngonegrmul  39081  crngm23  39139  hlrelat2  40663  pmaple  41021  pmodlem2  41107  dalaw  41146  sn-sup2  43759  syl5imp  45697  com3rgbi  45699  ee223  45819  relpmin  46148  2tceilhalfelfzo1  48621  iccpartigtl  48720  iccelpart  48730  lighneallem3  48907  bgoldbtbndlem3  49120  uhgrimisgrgric  49244  clnbgrgrim  49247  clnbgr3stgrgrlic  49333  gpgusgralem  49369  gpgvtxedg0  49376  gpgvtxedg1  49377  ply1mulgsumlem1  49713  fllog2  49895