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

Theorem adantrd 279
Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
Hypothesis
Ref Expression
adantrd.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
adantrd  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)

Proof of Theorem adantrd
StepHypRef Expression
1 simpl 109 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adantrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 32 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  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
This theorem is referenced by:  syldan  282  jaoa  720  prlem1  973  equveli  1759  elssabg  4145  suctr  4418  fvun1  5578  opabbrex  5913  poxp  6227  tposfo2  6262  1idprl  7577  1idpru  7578  uzind  9350  xrlttr  9779  fzen  10026  fz0fzelfz0  10110  fisumss  11381  fprodssdc  11579  zeqzmulgcd  11951  lcmgcdlem  12057  lcmdvds  12059  cncongr2  12084  exprmfct  12118  pceu  12275  infpnlem1  12337  ringadd2  13033  metrest  13666  bj-charfunbi  14212  bj-om  14338
  Copyright terms: Public domain W3C validator