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  7223  omxpenlem  7620  infxpabs  8595  domfin4  8694  isf32lem7  8742  ordpipq  9323  muladd  9996  lemul12b  10406  mulge0b  10419  qaddcl  11208  iooshf  11613  elfzomelpfzo  11895  expnegz  12181  bitsshft  14106  setscom  14643  catideu  15053  lubun  15731  grplmulf1o  16090  lidl1el  17844  frlmipval  18787  en2top  19464  cnpnei  19742  kgenidm  20025  ufileu  20397  fmfnfmlem4  20435  isngp4  21108  fsumcn  21351  evth  21436  mbfmulc2lem  22031  itg1addlem4  22083  dgreq0  22638  cxplt3  23057  cxple3  23058  basellem4  23333  axcontlem2  24244  usgra2adedgspth  24589  usghashecclwwlk  24811  grpoidinvlem3  25184  grpoideu  25187  grporcan  25199  3oalem2  26557  hmops  26915  adjadd  26988  mdslmd4i  27228  mdexchi  27230  mdsymlem1  27298  cvxscon  28665  poseq  29308  sltsolem1  29403  nodenselem5  29420  mblfinlem4  30029  ismblfin  30030  tailfb  30170  ismtyres  30279  ghomco  30320  rngoisocnv  30359  1idl  30398  srhmsubc  32617  srhmsubcOLD  32636  bnj607  33707  ps-2  34942
  Copyright terms: Public domain W3C validator