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:  fcof1o  5997  omwordri  7011  omxpenlem  7412  infxpabs  8381  domfin4  8480  isf32lem7  8528  ordpipq  9111  mulcmpblnr  9241  muladd  9777  lemul12b  10186  mulge0b  10199  qaddcl  10969  iooshf  11374  elfzomelpfzo  11629  expnegz  11898  bitsshft  13671  setscom  14204  catideu  14613  lubun  15293  grplmulf1o  15600  lidl1el  17300  en2top  18590  cnpnei  18868  kgenidm  19120  ufileu  19492  fmfnfmlem4  19530  isngp4  20203  fsumcn  20446  evth  20531  mbfmulc2lem  21125  itg1addlem4  21177  dgreq0  21732  cxplt3  22145  cxple3  22146  basellem4  22421  axcontlem2  23211  grpoidinvlem3  23693  grpoideu  23696  grporcan  23708  3oalem2  25066  hmops  25424  adjadd  25497  mdslmd4i  25737  mdexchi  25739  mdsymlem1  25807  cvxscon  27132  poseq  27714  sltsolem1  27809  nodenselem5  27826  mblfinlem4  28431  ismblfin  28432  tailfb  28598  ismtyres  28707  ghomco  28748  rngoisocnv  28787  1idl  28826  usgra2adedgspth  30305  usghashecclwwlk  30509  bnj607  31909  ps-2  33122
  Copyright terms: Public domain W3C validator