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  2907  fnsuppres  5748  cocan1  5817  ov6g  6001  dif1enOLD  7106  dif1en  7107  cfsmolem  7912  coftr  7915  axcc3  8080  axdc4lem  8097  gruf  8449  zdivmul  10100  coprmdvds  12797  lubss  14241  gsumccat  14480  odeq  14881  ghmplusg  15154  lmhmvsca  15818  elcls  16826  cnpresti  17032  cmpsublem  17142  ptpjcn  17321  elfm3  17661  rnelfmlem  17663  nmoix  18254  ig1pdvds  19578  coeid3  19638  amgm  20301  homco1  22397  hoadddi  22399  dedekindle  24098  br6  24185  brbtwn2  24605  colinearalg  24610  axsegconlem1  24617  ax5seglem1  24628  ax5seglem2  24629  bpolycl  24859  clfsebs  25450  isppm  25457  comppfsc  26410  upixp  26506  filbcmb  26535  mzprename  26930  infmrgelbi  27066  islindf4  27411  stoweidlem17  27869  3dim1  30278  llni  30319  lplni  30343  lvoli  30386  cdleme42mgN  31299
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