MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adantr2 Unicode version

Theorem 3adantr2 1156
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
Hypothesis
Ref Expression
3adantr.1
Assertion
Ref Expression
3adantr2

Proof of Theorem 3adantr2
StepHypRef Expression
1 3simpb 994 . 2
2 3adantr.1 . 2
31, 2sylan2 474 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3adant3r2  1206  po3nr  4819  sornom  8678  axdclem2  8921  issubc3  15218  pgpfi  16625  imasring  17268  prdslmodd  17615  icoopnst  21439  iocopnst  21440  axcontlem4  24270  constr2pth  24603  el2wlksotot  24882  usg2wlkonot  24883  usg2wotspth  24884  nvmdi  25545  mdsl3  27235  elicc3  30135  fzadd2  30234  iscringd  30396  dvmptfprodlem  31741  funcestrcsetclem9  32654  funcsetcestrclem9  32669  funcringcsetcOLD2lem9  32852  funcringcsetclem9OLD  32875  erngdvlem3  36716  erngdvlem3-rN  36724  dvalveclem  36752  dvhlveclem  36835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator