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

Theorem adantld 278
Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
Hypothesis
Ref Expression
adantld.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
adantld  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)

Proof of Theorem adantld
StepHypRef Expression
1 simpr 110 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 32 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  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-ia2 107
This theorem is referenced by:  jaoa  720  dedlema  969  dedlemb  970  prlem1  973  equveli  1759  poxp  6226  nnmordi  6510  eroprf  6621  xpdom2  6824  elni2  7291  prarloclemlo  7471  xrlttr  9769  fzen  10016  eluzgtdifelfzo  10170  ssfzo12bi  10198  climuni  11272  mulcn2  11291  serf0  11331  ntrivcvgap  11527  dfgcd2  11985  lcmgcdlem  12047  lcmdvds  12049  qnumdencl  12157  infpnlem1  12327  cnplimcim  13769  dveflem  13820  bj-charfundcALT  14183
  Copyright terms: Public domain W3C validator