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

Theorem adantld 274
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 109 . 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 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106
This theorem is referenced by:  jaoa  692  dedlema  936  dedlemb  937  prlem1  940  equveli  1715  poxp  6095  nnmordi  6378  eroprf  6488  xpdom2  6691  elni2  7086  prarloclemlo  7266  xrlttr  9521  fzen  9763  eluzgtdifelfzo  9914  ssfzo12bi  9942  climuni  11002  mulcn2  11021  serf0  11061  dfgcd2  11598  lcmgcdlem  11654  lcmdvds  11656  qnumdencl  11760  cnplimcim  12688  dveflem  12738
  Copyright terms: Public domain W3C validator