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  5511  fiunsnnn  6775  addcomnqg  7196  addassnqg  7197  nqtri3or  7211  lt2addnq  7219  lt2mulnq  7220  enq0ref  7248  enq0tr  7249  nqnq0pi  7253  nqpnq0nq  7268  nqnq0a  7269  distrnq0  7274  addassnq0lemcl  7276  ltsrprg  7562  mulcomsrg  7572  mulasssrg  7573  distrsrg  7574  aptisr  7594  mulcnsr  7650  cnegex  7947  sub4  8014  muladd  8153  ltleadd  8215  divdivdivap  8480  divadddivap  8494  ltmul12a  8625  fzrev  9871  facndiv  10492  cncongr1  11791  blbas  12612  cncfmet  12758  ptolemy  12915
  Copyright terms: Public domain W3C validator