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

Theorem ad2ant2rl 730
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 697 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 696 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  fcof1o  5965  omwordri  6751  omxpenlem  7145  infxpabs  8025  domfin4  8124  isf32lem7  8172  ordpipq  8752  mulcmpblnr  8882  muladd  9398  lemul12b  9799  qaddcl  10522  iooshf  10921  expnegz  11341  bitsshft  12914  setscom  13424  catideu  13827  lubun  14477  grplmulf1o  14792  lidl1el  16216  en2top  16973  cnpnei  17250  kgenidm  17500  ufileu  17872  fmfnfmlem4  17910  isngp4  18529  fsumcn  18771  evth  18855  mbfmulc2lem  19406  itg1addlem4  19458  dgreq0  20050  cxplt3  20458  cxple3  20459  basellem4  20733  grpoidinvlem3  21642  grpoideu  21645  grporcan  21657  3oalem2  23013  hmops  23371  adjadd  23444  mdslmd4i  23684  mdexchi  23686  mdsymlem1  23754  cvxscon  24709  mulge0b  24970  poseq  25277  sltsolem1  25346  nodenselem5  25363  axcontlem2  25618  tailfb  26097  ismtyres  26208  ghomco  26249  rngoisocnv  26288  1idl  26327  bnj607  28625  lubunNEW  29088  ps-2  29592
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 178  df-an 361
  Copyright terms: Public domain W3C validator