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

Theorem adantrl 469
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 284 1  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad2ant2l  499  ad2ant2rl  502  3ad2antr2  1132  3ad2antr3  1133  xordidc  1362  foco  5325  fvun1  5455  isocnv  5680  isores2  5682  f1oiso2  5696  offval  5957  xp2nd  6032  1stconst  6086  2ndconst  6087  tfrlem9  6184  nnmordi  6380  dom2lem  6634  fundmen  6668  mapen  6708  ssenen  6713  ltsonq  7174  ltexnqq  7184  genprndl  7297  genprndu  7298  ltpopr  7371  ltsopr  7372  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemdisj  7382  ltexprlemfl  7385  ltexprlemfu  7387  mulcmpblnrlemg  7516  cnegexlem2  7906  muladd  8114  eqord1  8213  eqord2  8214  divadddivap  8455  ltmul12a  8586  lemul12b  8587  cju  8687  zextlt  9111  supinfneg  9358  infsupneg  9359  xrre  9571  ixxdisj  9654  iooshf  9703  icodisj  9743  iccshftr  9745  iccshftl  9747  iccdil  9749  icccntr  9751  iccf1o  9755  fzaddel  9807  fzsubel  9808  seq3caopr  10224  expineg2  10270  expsubap  10309  expnbnd  10383  facndiv  10453  hashfacen  10547  lcmdvds  11687  hashdvds  11824  txlm  12375  blininf  12520  xmeter  12532  xmetresbl  12536  limcimo  12730
  Copyright terms: Public domain W3C validator