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

Theorem ad2ant2rl 730
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 697 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 696 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  fcof1o  6018  omwordri  6807  omxpenlem  7201  infxpabs  8084  domfin4  8183  isf32lem7  8231  ordpipq  8811  mulcmpblnr  8941  muladd  9458  lemul12b  9859  qaddcl  10582  iooshf  10981  expnegz  11406  bitsshft  12979  setscom  13489  catideu  13892  lubun  14542  grplmulf1o  14857  lidl1el  16281  en2top  17042  cnpnei  17320  kgenidm  17571  ufileu  17943  fmfnfmlem4  17981  isngp4  18650  fsumcn  18892  evth  18976  mbfmulc2lem  19531  itg1addlem4  19583  dgreq0  20175  cxplt3  20583  cxple3  20584  basellem4  20858  grpoidinvlem3  21786  grpoideu  21789  grporcan  21801  3oalem2  23157  hmops  23515  adjadd  23588  mdslmd4i  23828  mdexchi  23830  mdsymlem1  23898  cvxscon  24922  mulge0b  25183  poseq  25520  sltsolem1  25615  nodenselem5  25632  axcontlem2  25896  mblfinlem3  26236  ismblfin  26237  tailfb  26397  ismtyres  26508  ghomco  26549  rngoisocnv  26588  1idl  26627  elfzomelpfzo  28112  usgra2adedgspth  28268  bnj607  29224  lubunNEW  29708  ps-2  30212
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 178  df-an 361
  Copyright terms: Public domain W3C validator