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

Theorem adantrl 467
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 109 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 282 1  |-  ( (
ph  /\  ( th  /\  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:  ad2ant2l  497  ad2ant2rl  500  3ad2antr2  1130  3ad2antr3  1131  xordidc  1360  foco  5313  fvun1  5441  isocnv  5666  isores2  5668  f1oiso2  5682  offval  5943  xp2nd  6018  1stconst  6072  2ndconst  6073  tfrlem9  6170  nnmordi  6366  dom2lem  6620  fundmen  6654  mapen  6693  ssenen  6698  ltsonq  7151  ltexnqq  7161  genprndl  7274  genprndu  7275  ltpopr  7348  ltsopr  7349  ltexprlemm  7353  ltexprlemopl  7354  ltexprlemopu  7356  ltexprlemdisj  7359  ltexprlemfl  7362  ltexprlemfu  7364  mulcmpblnrlemg  7480  cnegexlem2  7858  muladd  8062  eqord1  8161  eqord2  8162  divadddivap  8397  ltmul12a  8525  lemul12b  8526  cju  8626  zextlt  9044  supinfneg  9289  infsupneg  9290  xrre  9493  ixxdisj  9576  iooshf  9625  icodisj  9665  iccshftr  9667  iccshftl  9669  iccdil  9671  icccntr  9673  iccf1o  9677  fzaddel  9729  fzsubel  9730  seq3caopr  10146  expineg2  10192  expsubap  10231  expnbnd  10305  facndiv  10375  hashfacen  10469  lcmdvds  11603  hashdvds  11739  txlm  12287  blininf  12410  xmeter  12422  xmetresbl  12426  limcimo  12587
  Copyright terms: Public domain W3C validator