ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2ant2lr Unicode version

Theorem ad2ant2lr 501
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2lr  |-  ( ( ( th  /\  ph )  /\  ( ps  /\  ta ) )  ->  ch )

Proof of Theorem ad2ant2lr
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrr 470 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantll 467 1  |-  ( ( ( th  /\  ph )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  mpteqb  5479  fiunsnnn  6743  addcomnqg  7157  addassnqg  7158  nqtri3or  7172  lt2addnq  7180  lt2mulnq  7181  enq0ref  7209  enq0tr  7210  nqnq0pi  7214  nqpnq0nq  7229  nqnq0a  7230  distrnq0  7235  addassnq0lemcl  7237  ltsrprg  7523  mulcomsrg  7533  mulasssrg  7534  distrsrg  7535  aptisr  7555  mulcnsr  7611  cnegex  7908  sub4  7975  muladd  8114  ltleadd  8176  divdivdivap  8441  divadddivap  8455  ltmul12a  8586  fzrev  9832  facndiv  10453  cncongr1  11711  blbas  12529  cncfmet  12675  ptolemy  12832
  Copyright terms: Public domain W3C validator