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  1276  ad5ant14  1299  ad5ant15  1300  ad5ant24  1302  ad5ant25  1303  ad5ant124  1308  ad5ant134  1310  ad5ant135  1311  rspct  3291  po2nr  5013  wefrc  5073  tz7.7  5713  funssres  5893  isomin  6547  f1ocnv2d  6846  onint  6949  f1oweALT  7104  bropfvvvv  7209  wfrlem12  7378  tfrlem9  7433  tz7.49  7492  oelim  7566  oaordex  7590  omordi  7598  omass  7612  oen0  7618  nnmass  7656  nnmordi  7663  inf3lem2  8477  epfrs  8558  indcardi  8815  ackbij1lem16  9008  cfcoflem  9045  axcc3  9211  zorn2lem7  9275  grur1a  9592  genpcd  9779  genpnmax  9780  mulclprlem  9792  distrlem1pr  9798  ltaddpr  9807  ltexprlem6  9814  ltexprlem7  9815  mulgt0sr  9877  divgt0  10842  divge0  10843  sup2  10930  uzind2  11421  uzwo  11702  supxrun  12096  expnbnd  12940  facdiv  13021  hashimarni  13173  swrdswrdlem  13404  wrd2ind  13422  s3iunsndisj  13648  caubnd  14039  dvdsabseq  14966  lcmfunsnlem2lem1  15282  divgcdcoprm0  15310  ncoprmlnprm  15367  cshwshashlem1  15733  psgnunilem4  17845  lmodvsdi  18814  xrsdsreclblem  19720  cpmatacl  20449  riinopn  20641  0ntr  20794  elcls  20796  hausnei2  21076  fgfil  21598  alexsubALTlem2  21771  alexsubALT  21774  aalioulem3  24006  aalioulem4  24007  wilthlem3  24709  upgrewlkle2  26385  upgrwlkdvdelem  26514  uhgrwkspthlem2  26532  1pthon2v  26892  n4cyclfrgr  27032  frgrnbnb  27034  frgrreg  27119  frgrregord013  27120  grpoidinvlem3  27227  elspansn5  28300  atcv1  29106  atcvatlem  29111  chirredlem3  29118  mdsymlem3  29131  mdsymlem5  29133  mdsymlem6  29134  sumdmdlem2  29145  f1o3d  29293  slmdvsdi  29571  frrlem11  31520  fgmin  32034  nndivsub  32125  mblfinlem3  33107  rngonegrmul  33402  crngm23  33460  hlrelat2  34196  pmaple  34554  pmodlem2  34640  dalaw  34679  syl5imp  38227  com3rgbi  38229  ee223  38368  iccpartigtl  40678  iccelpart  40688  lighneallem3  40844  bgoldbtbndlem3  41005  nzerooringczr  41381  ply1mulgsumlem1  41483  fllog2  41675
 Copyright terms: Public domain W3C validator