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

Theorem 3ad2antl2 1120
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 696 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl1 1113 1  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  fcofo  6021  cocan1  6024  ordiso2  7484  fin1a2lem9  8288  fin1a2lem12  8291  gchpwdom  8549  winainflem  8568  muldvds1  12874  ramcl  13397  gsumccat  14787  oddvdsnn0  15182  ghmplusg  15461  cnpnei  17328  qtopss  17747  elfm2  17980  flffbas  18027  cnpfcf  18073  deg1ldg  20015  nvmul0or  22133  hoadddi  23306  volfiniune  24586  funsseq  25393  brbtwn2  25844  colinearalg  25849  axsegconlem1  25856  bpolydif  26101  nn0prpwlem  26325  ssref  26363  fnemeet1  26395  keridl  26642  frlmsslss2  27222  frlmsslsp  27225  islindf4  27285  spthdifv  28309  2spontn0vne  28354  usgreghash2spot  28458  bnj548  29268  pmapglbx  30566  elpaddn0  30597  paddasslem9  30625  paddasslem10  30626  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