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  915  equveli  1684  elssabg  3949  suctr  4212  fvun1  5315  opabbrex  5628  poxp  5932  tposfo2  5964  1idprl  7052  1idpru  7053  uzind  8753  xrlttr  9160  fzen  9352  fz0fzelfz0  9429  zeqzmulgcd  10742  lcmgcdlem  10839  lcmdvds  10841  cncongr2  10866  exprmfct  10899  bj-om  11175
  Copyright terms: Public domain W3C validator