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

Theorem 3ad2antl2 1118
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antl2  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3ad2antl2
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantlr 695 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl1 1111 1  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  fcofo  5798  cocan1  5801  ordiso2  7230  fin1a2lem9  8034  fin1a2lem12  8037  gchpwdom  8296  winainflem  8315  muldvds1  12553  ramcl  13076  gsumccat  14464  oddvdsnn0  14859  ghmplusg  15138  cnpnei  16993  qtopss  17406  elfm2  17643  flffbas  17690  cnpfcf  17736  deg1ldg  19478  nvmul0or  21210  hoadddi  22383  funsseq  24125  brbtwn2  24533  colinearalg  24538  axsegconlem1  24545  bpolydif  24790  clfsebs  25347  flfnei2  25577  nn0prpwlem  26238  ssref  26283  fnemeet1  26315  keridl  26657  frlmsslss2  27245  frlmsslsp  27248  islindf4  27308  bnj548  28929  pmapglbx  29958  elpaddn0  29989  paddasslem9  30017  paddasslem10  30018  cdleme42mgN  30677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator