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

Theorem 3ad2antl3 1121
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 695 . 2  |-  ( ( ( ta  /\  ph )  /\  ch )  ->  th )
323adantl1 1113 1  |-  ( ( ( ps  /\  ta  /\ 
ph )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  rspc3ev  3062  brcogw  5041  fnsuppres  5952  cocan1  6024  ov6g  6211  dif1enOLD  7340  dif1en  7341  cfsmolem  8150  coftr  8153  axcc3  8318  axdc4lem  8335  gruf  8686  zdivmul  10342  coprmdvds  13102  lubss  14548  gsumccat  14787  odeq  15188  ghmplusg  15461  lmhmvsca  16121  elcls  17137  cnpresti  17352  cmpsublem  17462  ptpjcn  17643  elfm3  17982  rnelfmlem  17984  nmoix  18763  ig1pdvds  20099  coeid3  20159  amgm  20829  usgra2edg  21402  homco1  23304  hoadddi  23306  dedekindle  25188  br6  25380  brbtwn2  25844  colinearalg  25849  axsegconlem1  25856  ax5seglem1  25867  ax5seglem2  25868  bpolycl  26098  comppfsc  26387  upixp  26431  filbcmb  26442  mzprename  26806  infmrgelbi  26941  islindf4  27285  stoweidlem17  27742  stoweidlem28  27753  3dim1  30264  llni  30305  lplni  30329  lvoli  30372  cdleme42mgN  31285
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator