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

Theorem adantrd 273
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 107 . 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 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem is referenced by:  syldan  276  jaoa  673  prlem1  917  equveli  1686  elssabg  3961  suctr  4224  fvun1  5335  opabbrex  5652  poxp  5956  tposfo2  5988  1idprl  7096  1idpru  7097  uzind  8793  xrlttr  9200  fzen  9392  fz0fzelfz0  9469  fisumss  10675  zeqzmulgcd  10868  lcmgcdlem  10965  lcmdvds  10967  cncongr2  10992  exprmfct  11025  bj-om  11301
  Copyright terms: Public domain W3C validator