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

Theorem ad2ant2rl 731
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 698 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 697 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  fcof1o  6028  omwordri  6817  omxpenlem  7211  infxpabs  8094  domfin4  8193  isf32lem7  8241  ordpipq  8821  mulcmpblnr  8951  muladd  9468  lemul12b  9869  qaddcl  10592  iooshf  10991  expnegz  11416  bitsshft  12989  setscom  13499  catideu  13902  lubun  14552  grplmulf1o  14867  lidl1el  16291  en2top  17052  cnpnei  17330  kgenidm  17581  ufileu  17953  fmfnfmlem4  17991  isngp4  18660  fsumcn  18902  evth  18986  mbfmulc2lem  19541  itg1addlem4  19593  dgreq0  20185  cxplt3  20593  cxple3  20594  basellem4  20868  grpoidinvlem3  21796  grpoideu  21799  grporcan  21811  3oalem2  23167  hmops  23525  adjadd  23598  mdslmd4i  23838  mdexchi  23840  mdsymlem1  23908  cvxscon  24932  mulge0b  25193  poseq  25530  sltsolem1  25625  nodenselem5  25642  axcontlem2  25906  mblfinlem4  26248  ismblfin  26249  tailfb  26408  ismtyres  26519  ghomco  26560  rngoisocnv  26599  1idl  26638  elfzomelpfzo  28140  usgra2adedgspth  28341  bnj607  29349  lubunNEW  29833  ps-2  30337
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 179  df-an 362
  Copyright terms: Public domain W3C validator