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  6236  nnmordi  6520  eroprf  6631  xpdom2  6834  elni2  7316  prarloclemlo  7496  xrlttr  9798  fzen  10046  eluzgtdifelfzo  10200  ssfzo12bi  10228  climuni  11304  mulcn2  11323  serf0  11363  ntrivcvgap  11559  dfgcd2  12018  lcmgcdlem  12080  lcmdvds  12082  qnumdencl  12190  infpnlem1  12360  cnplimcim  14276  dveflem  14327  bj-charfundcALT  14701
  Copyright terms: Public domain W3C validator