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

Theorem ad2ant2rl 748
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 715 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 714 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  omwordri  7211  omxpenlem  7608  infxpabs  8581  domfin4  8680  isf32lem7  8728  ordpipq  9309  muladd  9978  lemul12b  10388  mulge0b  10401  qaddcl  11187  iooshf  11592  elfzomelpfzo  11871  expnegz  12155  bitsshft  13973  setscom  14509  catideu  14919  lubun  15599  grplmulf1o  15906  lidl1el  17641  en2top  19246  cnpnei  19524  kgenidm  19776  ufileu  20148  fmfnfmlem4  20186  isngp4  20859  fsumcn  21102  evth  21187  mbfmulc2lem  21782  itg1addlem4  21834  dgreq0  22389  cxplt3  22802  cxple3  22803  basellem4  23078  axcontlem2  23937  usgra2adedgspth  24275  usghashecclwwlk  24497  grpoidinvlem3  24870  grpoideu  24873  grporcan  24885  3oalem2  26243  hmops  26601  adjadd  26674  mdslmd4i  26914  mdexchi  26916  mdsymlem1  26984  cvxscon  28314  poseq  28896  sltsolem1  28991  nodenselem5  29008  mblfinlem4  29618  ismblfin  29619  tailfb  29785  ismtyres  29894  ghomco  29935  rngoisocnv  29974  1idl  30013  bnj607  32928  ps-2  34149
  Copyright terms: Public domain W3C validator