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

Theorem adantrl 462
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantrl  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )

Proof of Theorem adantrl
StepHypRef Expression
1 simpr 108 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 280 1  |-  ( (
ph  /\  ( th  /\  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:  ad2ant2l  492  ad2ant2rl  495  3ad2antr2  1105  3ad2antr3  1106  xordidc  1331  foco  5147  fvun1  5271  isocnv  5482  isores2  5484  f1oiso2  5497  offval  5750  xp2nd  5824  1stconst  5873  2ndconst  5874  tfrlem9  5968  nnmordi  6155  dom2lem  6319  fundmen  6353  ltsonq  6650  ltexnqq  6660  genprndl  6773  genprndu  6774  ltpopr  6847  ltsopr  6848  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemdisj  6858  ltexprlemfl  6861  ltexprlemfu  6863  mulcmpblnrlemg  6979  cnegexlem2  7351  muladd  7555  divadddivap  7882  ltmul12a  8005  lemul12b  8006  cju  8105  zextlt  8520  supinfneg  8764  infsupneg  8765  xrre  8963  ixxdisj  9002  iooshf  9051  icodisj  9090  iccshftr  9092  iccshftl  9094  iccdil  9096  icccntr  9098  iccf1o  9102  fzaddel  9153  fzsubel  9154  iseqcaopr  9558  expineg2  9582  expsubap  9621  expnbnd  9693  facndiv  9763  lcmdvds  10605
  Copyright terms: Public domain W3C validator