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

Theorem ad2ant2lr 494
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 463 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantll 460 1  |-  ( ( ( th  /\  ph )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  mpteqb  5393  fiunsnnn  6595  addcomnqg  6938  addassnqg  6939  nqtri3or  6953  lt2addnq  6961  lt2mulnq  6962  enq0ref  6990  enq0tr  6991  nqnq0pi  6995  nqpnq0nq  7010  nqnq0a  7011  distrnq0  7016  addassnq0lemcl  7018  ltsrprg  7291  mulcomsrg  7301  mulasssrg  7302  distrsrg  7303  aptisr  7322  mulcnsr  7370  cnegex  7658  sub4  7725  muladd  7860  ltleadd  7922  divdivdivap  8178  divadddivap  8192  ltmul12a  8319  fzrev  9494  facndiv  10143  cncongr1  11359
  Copyright terms: Public domain W3C validator