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  4149  suctr  4422  fvun1  5583  opabbrex  5919  poxp  6233  tposfo2  6268  1idprl  7589  1idpru  7590  uzind  9364  xrlttr  9795  fzen  10043  fz0fzelfz0  10127  fisumss  11400  fprodssdc  11598  zeqzmulgcd  11971  lcmgcdlem  12077  lcmdvds  12079  cncongr2  12104  exprmfct  12138  pceu  12295  infpnlem1  12357  ringadd2  13210  metrest  14009  bj-charfunbi  14566  bj-om  14692
  Copyright terms: Public domain W3C validator