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

Theorem ad2ant2rl 495
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 462 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 461 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  fvtp1g  5505  fcof1o  5568  infnfi  6611  addcomnqg  6940  addassnqg  6941  nqtri3or  6955  ltexnqq  6967  nqnq0pi  6997  nqpnq0nq  7012  nqnq0a  7013  addassnq0lemcl  7020  ltaddpr  7156  ltexprlemloc  7166  addcanprlemu  7174  recexprlem1ssu  7193  aptiprleml  7198  mulcomsrg  7303  mulasssrg  7304  distrsrg  7305  aptisr  7324  mulcnsr  7372  cnegex  7660  muladd  7862  lemul12b  8322  qaddcl  9120  iooshf  9370  elfzomelpfzo  9642  expnegzap  9989  setscom  11534
  Copyright terms: Public domain W3C validator