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

Theorem 3ad2antl2 1159
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 1152 1  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  fcofo  6190  cocan1  6193  ordiso2  7952  fin1a2lem9  8800  fin1a2lem12  8803  gchpwdom  9060  winainflem  9083  muldvds1  13886  ramcl  14423  gsumccat  15881  oddvdsnn0  16441  ghmplusg  16725  frlmsslss2  18674  frlmsslss2OLD  18675  frlmsslsp  18698  frlmsslspOLD  18699  islindf4  18742  mamures  18761  matepmcl  18833  matepm2cl  18834  pmatcollpw2lem  19147  cnpnei  19633  ssref  19881  qtopss  20084  elfm2  20317  flffbas  20364  cnpfcf  20410  deg1ldg  22360  brbtwn2  24022  colinearalg  24027  axsegconlem1  24034  clwwlkf  24608  2spontn0vne  24701  usgreghash2spot  24884  nvmul0or  25361  hoadddi  26536  volfiniune  28018  funsseq  29117  bpolydif  29735  nn0prpwlem  30058  fnemeet1  30102  keridl  30347  lcmdvds  31129  lptre2pt  31496  fourierdlem42  31763  fourierdlem48  31769  fourierdlem54  31775  fourierdlem77  31798  spthdifv  32133  bnj548  33390  pmapglbx  34921  elpaddn0  34952  paddasslem9  34980  paddasslem10  34981  cdleme42mgN  35640
  Copyright terms: Public domain W3C validator