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

Theorem ad2ant2rl 500
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 467 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 466 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  fvtp1g  5582  fcof1o  5644  infnfi  6742  addcomnqg  7134  addassnqg  7135  nqtri3or  7149  ltexnqq  7161  nqnq0pi  7191  nqpnq0nq  7206  nqnq0a  7207  addassnq0lemcl  7214  ltaddpr  7350  ltexprlemloc  7360  addcanprlemu  7368  recexprlem1ssu  7387  aptiprleml  7392  mulcomsrg  7497  mulasssrg  7498  distrsrg  7499  aptisr  7518  mulcnsr  7567  cnegex  7860  muladd  8062  lemul12b  8526  qaddcl  9326  iooshf  9625  elfzomelpfzo  9898  expnegzap  10217  setscom  11839  cnpnei  12227
  Copyright terms: Public domain W3C validator