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

Theorem ad2ant2rl 511
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 478 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantlr 477 1  |-  ( ( ( ph  /\  th )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  fvtp1g  5767  fcof1o  5833  infnfi  6953  addcomnqg  7443  addassnqg  7444  nqtri3or  7458  ltexnqq  7470  nqnq0pi  7500  nqpnq0nq  7515  nqnq0a  7516  addassnq0lemcl  7523  ltaddpr  7659  ltexprlemloc  7669  addcanprlemu  7677  recexprlem1ssu  7696  aptiprleml  7701  mulcomsrg  7819  mulasssrg  7820  distrsrg  7821  aptisr  7841  mulcnsr  7897  cnegex  8199  muladd  8405  lemul12b  8882  qaddcl  9703  iooshf  10021  elfzomelpfzo  10301  expnegzap  10647  setscom  12661  grplmulf1o  13149  lmodfopne  13825  cnpnei  14398  cxplt3  15095  cxple3  15096
  Copyright terms: Public domain W3C validator