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

Theorem ad2ant2rl 729
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2rl  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )

Proof of Theorem ad2ant2rl
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrl 696 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 695 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  fcof1o  5805  omwordri  6572  omxpenlem  6965  infxpabs  7840  domfin4  7939  isf32lem7  7987  ordpipq  8568  mulcmpblnr  8698  muladd  9214  lemul12b  9615  qaddcl  10334  iooshf  10730  expnegz  11138  bitsshft  12668  setscom  13178  catideu  13579  lubun  14229  grplmulf1o  14544  lidl1el  15972  en2top  16725  cnpnei  16995  kgenidm  17244  ufileu  17616  fmfnfmlem4  17654  isngp4  18135  fsumcn  18376  evth  18459  mbfmulc2lem  19004  itg1addlem4  19056  dgreq0  19648  cxplt3  20049  cxple3  20050  basellem4  20323  grpoidinvlem3  20875  grpoideu  20878  grporcan  20890  3oalem2  22244  hmops  22602  adjadd  22675  mdslmd4i  22915  mdexchi  22917  mdsymlem1  22985  cvxscon  23776  mulge0b  24088  poseq  24255  sltsolem1  24324  nodenselem5  24341  axcontlem2  24595  cbicp  25177  tailfb  26337  ismtyres  26543  ghomco  26584  rngoisocnv  26623  1idl  26662  bnj607  29021  lubunNEW  29236  ps-2  29740
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
  Copyright terms: Public domain W3C validator