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

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

Proof of Theorem 3ad2antl3
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantll 694 . 2  |-  ( ( ( ta  /\  ph )  /\  ch )  ->  th )
323adantl1 1111 1  |-  ( ( ( ps  /\  ta  /\ 
ph )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  rspc3ev  2894  fnsuppres  5732  cocan1  5801  ov6g  5985  dif1enOLD  7090  dif1en  7091  cfsmolem  7896  coftr  7899  axcc3  8064  axdc4lem  8081  gruf  8433  zdivmul  10084  coprmdvds  12781  lubss  14225  gsumccat  14464  odeq  14865  ghmplusg  15138  lmhmvsca  15802  elcls  16810  cnpresti  17016  cmpsublem  17126  ptpjcn  17305  elfm3  17645  rnelfmlem  17647  nmoix  18238  ig1pdvds  19562  coeid3  19622  amgm  20285  homco1  22381  hoadddi  22383  dedekindle  24083  br6  24114  brbtwn2  24533  colinearalg  24538  axsegconlem1  24545  ax5seglem1  24556  ax5seglem2  24557  bpolycl  24787  clfsebs  25347  isppm  25354  comppfsc  26307  upixp  26403  filbcmb  26432  mzprename  26827  infmrgelbi  26963  islindf4  27308  stoweidlem17  27766  3dim1  29656  llni  29697  lplni  29721  lvoli  29764  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