MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com34 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 com4.1 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
2 pm2.04 90 . 2 ((𝜒 → (𝜃𝜏)) → (𝜃 → (𝜒𝜏)))
31, 2syl6 35 1 (𝜑 → (𝜓 → (𝜃 → (𝜒𝜏))))
Colors of variables: wff setvar class
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  1356  rspct  3584  po2nr  5464  wefrc  5526  tz7.7  6195  funssres  6377  isomin  7074  f1ocnv2d  7383  onint  7495  f1oweALT  7659  bropfvvvv  7774  wfrlem12  7953  tfrlem9  8008  tz7.49  8068  oelim  8146  oaordex  8171  omordi  8179  omass  8193  oen0  8199  nnmass  8237  nnmordi  8244  inf3lem2  9080  epfrs  9161  indcardi  9456  ackbij1lem16  9646  cfcoflem  9683  axcc3  9849  zorn2lem7  9913  grur1a  10230  genpcd  10417  genpnmax  10418  mulclprlem  10430  distrlem1pr  10436  ltaddpr  10445  ltexprlem6  10452  ltexprlem7  10453  mulgt0sr  10516  divgt0  11497  divge0  11498  sup2  11584  uzind2  12063  uzwo  12299  supxrun  12697  expnbnd  13589  facdiv  13643  hashimarni  13798  swrdswrdlem  14057  wrd2ind  14076  s3iunsndisj  14319  caubnd  14709  dvdsabseq  15654  lcmfunsnlem2lem1  15971  divgcdcoprm0  15998  ncoprmlnprm  16057  cshwshashlem1  16420  psgnunilem4  18616  lmodvsdi  19648  xrsdsreclblem  20135  cpmatacl  21319  riinopn  21511  0ntr  21674  elcls  21676  hausnei2  21956  fgfil  22478  alexsubALTlem2  22651  alexsubALT  22654  aalioulem3  24928  aalioulem4  24929  wilthlem3  25653  2sqreultlem  26029  2sqreunnltlem  26032  finsumvtxdg2size  27338  upgrewlkle2  27394  upgrwlkdvdelem  27523  uhgrwkspthlem2  27541  clwwlkinwwlk  27823  wwlksext2clwwlk  27840  1pthon2v  27936  n4cyclfrgr  28074  frgrnbnb  28076  frgrwopreglem4a  28093  frgrreg  28177  frgrregord013  28178  grpoidinvlem3  28287  elspansn5  29355  atcv1  30161  atcvatlem  30166  chirredlem3  30173  mdsymlem3  30186  mdsymlem5  30188  mdsymlem6  30189  sumdmdlem2  30200  f1o3d  30380  slmdvsdi  30874  satfv0fun  32692  satffunlem1lem1  32723  satffunlem2lem1  32725  fgmin  33792  nndivsub  33879  mblfinlem3  35054  rngonegrmul  35340  crngm23  35398  hlrelat2  36657  pmaple  37015  pmodlem2  37101  dalaw  37140  syl5imp  41152  com3rgbi  41154  ee223  41274  iccpartigtl  43879  iccelpart  43889  lighneallem3  44064  bgoldbtbndlem3  44264  isomgrsym  44293  isomgrtr  44296  nzerooringczr  44635  ply1mulgsumlem1  44733  fllog2  44921
  Copyright terms: Public domain W3C validator