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

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

Proof of Theorem ad2ant2rl
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrl 455 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 454 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  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:  fvtp1g  5397  fcof1o  5457  addcomnqg  6537  addassnqg  6538  nqtri3or  6552  ltexnqq  6564  nqnq0pi  6594  nqpnq0nq  6609  nqnq0a  6610  addassnq0lemcl  6617  ltaddpr  6753  ltexprlemloc  6763  addcanprlemu  6771  recexprlem1ssu  6790  aptiprleml  6795  mulcomsrg  6900  mulasssrg  6901  distrsrg  6902  aptisr  6921  mulcnsr  6969  cnegex  7252  muladd  7453  lemul12b  7902  qaddcl  8667  iooshf  8922  elfzomelpfzo  9189  expnegzap  9454
  Copyright terms: Public domain W3C validator