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  5803  omwordri  6570  omxpenlem  6963  infxpabs  7838  domfin4  7937  isf32lem7  7985  ordpipq  8566  mulcmpblnr  8696  muladd  9212  lemul12b  9613  qaddcl  10332  iooshf  10728  expnegz  11136  bitsshft  12666  setscom  13176  catideu  13577  lubun  14227  grplmulf1o  14542  lidl1el  15970  en2top  16723  cnpnei  16993  kgenidm  17242  ufileu  17614  fmfnfmlem4  17652  isngp4  18133  fsumcn  18374  evth  18457  mbfmulc2lem  19002  itg1addlem4  19054  dgreq0  19646  cxplt3  20047  cxple3  20048  basellem4  20321  grpoidinvlem3  20873  grpoideu  20876  grporcan  20888  3oalem2  22242  hmops  22600  adjadd  22673  mdslmd4i  22913  mdexchi  22915  mdsymlem1  22983  cvxscon  23774  mulge0b  24086  poseq  24253  sltsolem1  24322  nodenselem5  24339  axcontlem2  24593  cbicp  25166  tailfb  26326  ismtyres  26532  ghomco  26573  rngoisocnv  26612  1idl  26651  bnj607  28948  lubunNEW  29163  ps-2  29667
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