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

Theorem adantld 272
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 108 . 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 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105
This theorem is referenced by:  jaoa  675  dedlema  915  dedlemb  916  prlem1  919  equveli  1689  poxp  5997  nnmordi  6275  eroprf  6385  xpdom2  6547  elni2  6873  prarloclemlo  7053  xrlttr  9265  fzen  9457  eluzgtdifelfzo  9608  ssfzo12bi  9636  climuni  10681  mulcn2  10701  serf0  10741  dfgcd2  11281  lcmgcdlem  11337  lcmdvds  11339  qnumdencl  11443
  Copyright terms: Public domain W3C validator