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  5765  omwordri  6566  omxpenlem  6959  infxpabs  7834  domfin4  7933  isf32lem7  7981  ordpipq  8562  mulcmpblnr  8692  muladd  9208  lemul12b  9609  qaddcl  10328  iooshf  10724  expnegz  11132  bitsshft  12662  setscom  13172  catideu  13573  lubun  14223  grplmulf1o  14538  lidl1el  15966  en2top  16719  cnpnei  16989  kgenidm  17238  ufileu  17610  fmfnfmlem4  17648  isngp4  18129  fsumcn  18370  evth  18453  mbfmulc2lem  18998  itg1addlem4  19050  dgreq0  19642  cxplt3  20043  cxple3  20044  basellem4  20317  grpoidinvlem3  20867  grpoideu  20870  grporcan  20882  3oalem2  22238  hmops  22596  adjadd  22669  mdslmd4i  22909  mdexchi  22911  mdsymlem1  22979  cvxscon  23181  mulge0b  23492  poseq  23657  axsltsolem1  23725  axdenselem5  23743  axcontlem2  24003  cbicp  24577  tailfb  25737  ismtyres  25943  ghomco  25984  rngoisocnv  26023  1idl  26062  bnj607  28227  lubunNEW  28442  ps-2  28946
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