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

Theorem ad2ant2lr 487
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 456 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantll 453 1  |-  ( ( ( th  /\  ph )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  mpteqb  5289  fiunsnnn  6369  addcomnqg  6537  addassnqg  6538  nqtri3or  6552  lt2addnq  6560  lt2mulnq  6561  enq0ref  6589  enq0tr  6590  nqnq0pi  6594  nqpnq0nq  6609  nqnq0a  6610  distrnq0  6615  addassnq0lemcl  6617  ltsrprg  6890  mulcomsrg  6900  mulasssrg  6901  distrsrg  6902  aptisr  6921  mulcnsr  6969  cnegex  7252  sub4  7319  muladd  7453  ltleadd  7515  divdivdivap  7764  divadddivap  7778  ltmul12a  7901  fzrev  9048  facndiv  9607
  Copyright terms: Public domain W3C validator