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

Theorem 3ad2antl2 1151
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 714 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl1 1144 1  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  fcofo  6104  cocan1  6107  ordiso2  7843  fin1a2lem9  8691  fin1a2lem12  8694  gchpwdom  8951  winainflem  8974  muldvds1  13678  ramcl  14211  gsumccat  15641  oddvdsnn0  16171  ghmplusg  16452  frlmsslss2  18327  frlmsslss2OLD  18328  frlmsslsp  18351  frlmsslspOLD  18352  islindf4  18395  mamures  18418  matepmcl  18477  matepm2cl  18478  cnpnei  19003  qtopss  19423  elfm2  19656  flffbas  19703  cnpfcf  19749  deg1ldg  21699  brbtwn2  23323  colinearalg  23328  axsegconlem1  23335  nvmul0or  24204  hoadddi  25379  volfiniune  26810  funsseq  27744  bpolydif  28362  nn0prpwlem  28685  ssref  28723  fnemeet1  28755  keridl  29000  spthdifv  30467  2spontn0vne  30574  clwwlkf  30624  usgreghash2spot  30830  pmatcollpw2lem  31284  bnj548  32242  pmapglbx  33771  elpaddn0  33802  paddasslem9  33830  paddasslem10  33831  cdleme42mgN  34490
  Copyright terms: Public domain W3C validator