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

Theorem 3ad2antl2 1118
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 695 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl1 1111 1  |-  ( ( ( ps  /\  ph  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  fcofo  5814  cocan1  5817  ordiso2  7246  fin1a2lem9  8050  fin1a2lem12  8053  gchpwdom  8312  winainflem  8331  muldvds1  12569  ramcl  13092  gsumccat  14480  oddvdsnn0  14875  ghmplusg  15154  cnpnei  17009  qtopss  17422  elfm2  17659  flffbas  17706  cnpfcf  17752  deg1ldg  19494  nvmul0or  21226  hoadddi  22399  funsseq  24196  brbtwn2  24605  colinearalg  24610  axsegconlem1  24617  bpolydif  24862  clfsebs  25450  flfnei2  25680  nn0prpwlem  26341  ssref  26386  fnemeet1  26418  keridl  26760  frlmsslss2  27348  frlmsslsp  27351  islindf4  27411  bnj548  29245  pmapglbx  30580  elpaddn0  30611  paddasslem9  30639  paddasslem10  30640  cdleme42mgN  31299
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator