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  4150  suctr  4423  fvun1  5584  opabbrex  5921  poxp  6235  tposfo2  6270  1idprl  7591  1idpru  7592  uzind  9366  xrlttr  9797  fzen  10045  fz0fzelfz0  10129  fisumss  11402  fprodssdc  11600  zeqzmulgcd  11973  lcmgcdlem  12079  lcmdvds  12081  cncongr2  12106  exprmfct  12140  pceu  12297  infpnlem1  12359  ringadd2  13215  metrest  14045  bj-charfunbi  14602  bj-om  14728
  Copyright terms: Public domain W3C validator