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  3an1rsOLD  1301  3an1rs  1312  ad5ant14OLD  1335  ad5ant15OLD  1337  ad5ant24OLD  1341  ad5ant25OLD  1343  ad5ant124  1351  ad5ant134  1353  ad5ant135  1354  rspct  3333  po2nr  5077  wefrc  5137  tz7.7  5787  funssres  5968  isomin  6627  f1ocnv2d  6928  onint  7037  f1oweALT  7194  bropfvvvv  7302  wfrlem12  7471  tfrlem9  7526  tz7.49  7585  oelim  7659  oaordex  7683  omordi  7691  omass  7705  oen0  7711  nnmass  7749  nnmordi  7756  inf3lem2  8564  epfrs  8645  indcardi  8902  ackbij1lem16  9095  cfcoflem  9132  axcc3  9298  zorn2lem7  9362  grur1a  9679  genpcd  9866  genpnmax  9867  mulclprlem  9879  distrlem1pr  9885  ltaddpr  9894  ltexprlem6  9901  ltexprlem7  9902  mulgt0sr  9964  divgt0  10929  divge0  10930  sup2  11017  uzind2  11508  uzwo  11789  supxrun  12184  expnbnd  13033  facdiv  13114  hashimarni  13266  swrdswrdlem  13505  wrd2ind  13523  s3iunsndisj  13753  caubnd  14142  dvdsabseq  15082  lcmfunsnlem2lem1  15398  divgcdcoprm0  15426  ncoprmlnprm  15483  cshwshashlem1  15849  psgnunilem4  17963  lmodvsdi  18934  xrsdsreclblem  19840  cpmatacl  20569  riinopn  20761  0ntr  20923  elcls  20925  hausnei2  21205  fgfil  21726  alexsubALTlem2  21899  alexsubALT  21902  aalioulem3  24134  aalioulem4  24135  wilthlem3  24841  finsumvtxdg2size  26502  upgrewlkle2  26558  upgrwlkdvdelem  26688  uhgrwkspthlem2  26706  clwwlkinwwlk  27003  wwlksext2clwwlk  27021  1pthon2v  27131  n4cyclfrgr  27271  frgrnbnb  27273  frgrwopreglem4a  27290  frgrreg  27381  frgrregord013  27382  grpoidinvlem3  27488  elspansn5  28561  atcv1  29367  atcvatlem  29372  chirredlem3  29379  mdsymlem3  29392  mdsymlem5  29394  mdsymlem6  29395  sumdmdlem2  29406  f1o3d  29559  slmdvsdi  29896  fgmin  32490  nndivsub  32581  mblfinlem3  33578  rngonegrmul  33873  crngm23  33931  hlrelat2  35007  pmaple  35365  pmodlem2  35451  dalaw  35490  syl5imp  39035  com3rgbi  39037  ee223  39176  iccpartigtl  41684  iccelpart  41694  lighneallem3  41849  bgoldbtbndlem3  42020  nzerooringczr  42397  ply1mulgsumlem1  42499  fllog2  42687
  Copyright terms: Public domain W3C validator