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  673  dedlema  911  dedlemb  912  prlem1  915  equveli  1684  poxp  5905  nnmordi  6177  eroprf  6287  xpdom2  6397  elni2  6636  prarloclemlo  6816  xrlttr  9016  fzen  9208  eluzgtdifelfzo  9353  ssfzo12bi  9381  climuni  10351  mulcn2  10370  serif0  10408  dfgcd2  10628  lcmgcdlem  10684  lcmdvds  10686  qnumdencl  10790
  Copyright terms: Public domain W3C validator