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

Theorem 3ad2antl2 1160
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 1153 1  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  fcofo  6176  cocan1  6179  ordiso2  7943  fin1a2lem9  8791  fin1a2lem12  8794  gchpwdom  9051  winainflem  9074  muldvds1  13885  ramcl  14424  gsumccat  15883  oddvdsnn0  16442  ghmplusg  16726  frlmsslss2  18678  frlmsslss2OLD  18679  frlmsslsp  18702  frlmsslspOLD  18703  islindf4  18746  mamures  18765  matepmcl  18837  matepm2cl  18838  pmatcollpw2lem  19151  cnpnei  19638  ssref  19886  qtopss  20089  elfm2  20322  flffbas  20369  cnpfcf  20415  deg1ldg  22365  brbtwn2  24080  colinearalg  24085  axsegconlem1  24092  clwwlkf  24666  2spontn0vne  24759  usgreghash2spot  24941  nvmul0or  25419  hoadddi  26594  volfiniune  28075  funsseq  29174  bpolydif  29792  nn0prpwlem  30115  fnemeet1  30159  keridl  30404  lcmdvds  31190  lptre2pt  31554  fourierdlem42  31820  fourierdlem48  31826  fourierdlem54  31832  fourierdlem77  31855  spthdifv  32190  bnj548  33688  pmapglbx  35233  elpaddn0  35264  paddasslem9  35292  paddasslem10  35293  cdleme42mgN  35954
  Copyright terms: Public domain W3C validator