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  5987  cocan1  5990  ordiso2  7721  fin1a2lem9  8569  fin1a2lem12  8572  gchpwdom  8829  winainflem  8852  muldvds1  13549  ramcl  14082  gsumccat  15510  oddvdsnn0  16038  ghmplusg  16319  frlmsslss2  18174  frlmsslss2OLD  18175  frlmsslsp  18198  frlmsslspOLD  18199  islindf4  18242  mamures  18265  matepmcl  18322  matepm2cl  18323  cnpnei  18843  qtopss  19263  elfm2  19496  flffbas  19543  cnpfcf  19589  deg1ldg  21538  brbtwn2  23102  colinearalg  23107  axsegconlem1  23114  nvmul0or  23983  hoadddi  25158  volfiniune  26598  funsseq  27531  bpolydif  28149  nn0prpwlem  28470  ssref  28508  fnemeet1  28540  keridl  28785  spthdifv  30252  2spontn0vne  30359  clwwlkf  30409  usgreghash2spot  30615  bnj548  31777  pmapglbx  33253  elpaddn0  33284  paddasslem9  33312  paddasslem10  33313  cdleme42mgN  33972
  Copyright terms: Public domain W3C validator