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

Theorem ad2ant2lr 507
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 476 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantll 473 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  5586  fiunsnnn  6859  addcomnqg  7343  addassnqg  7344  nqtri3or  7358  lt2addnq  7366  lt2mulnq  7367  enq0ref  7395  enq0tr  7396  nqnq0pi  7400  nqpnq0nq  7415  nqnq0a  7416  distrnq0  7421  addassnq0lemcl  7423  ltsrprg  7709  mulcomsrg  7719  mulasssrg  7720  distrsrg  7721  aptisr  7741  mulcnsr  7797  cnegex  8097  sub4  8164  muladd  8303  ltleadd  8365  divdivdivap  8630  divadddivap  8644  ltmul12a  8776  fzrev  10040  facndiv  10673  cncongr1  12057  blbas  13227  cncfmet  13373  ptolemy  13539
  Copyright terms: Public domain W3C validator