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  5819  omwordri  6586  omxpenlem  6979  infxpabs  7854  domfin4  7953  isf32lem7  8001  ordpipq  8582  mulcmpblnr  8712  muladd  9228  lemul12b  9629  qaddcl  10348  iooshf  10744  expnegz  11152  bitsshft  12682  setscom  13192  catideu  13593  lubun  14243  grplmulf1o  14558  lidl1el  15986  en2top  16739  cnpnei  17009  kgenidm  17258  ufileu  17630  fmfnfmlem4  17668  isngp4  18149  fsumcn  18390  evth  18473  mbfmulc2lem  19018  itg1addlem4  19070  dgreq0  19662  cxplt3  20063  cxple3  20064  basellem4  20337  grpoidinvlem3  20889  grpoideu  20892  grporcan  20904  3oalem2  22258  hmops  22616  adjadd  22689  mdslmd4i  22929  mdexchi  22931  mdsymlem1  22999  cvxscon  23789  mulge0b  24101  poseq  24324  sltsolem1  24393  nodenselem5  24410  axcontlem2  24665  cbicp  25269  tailfb  26429  ismtyres  26635  ghomco  26676  rngoisocnv  26715  1idl  26754  bnj607  29264  lubunNEW  29785  ps-2  30289
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