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

Theorem adantld 276
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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
adantld (𝜑 → ((𝜃𝜓) → 𝜒))

Proof of Theorem adantld
StepHypRef Expression
1 simpr 109 . 2 ((𝜃𝜓) → 𝜓)
2 adantld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 32 1 (𝜑 → ((𝜃𝜓) → 𝜒))
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  694  dedlema  938  dedlemb  939  prlem1  942  equveli  1717  poxp  6097  nnmordi  6380  eroprf  6490  xpdom2  6693  elni2  7090  prarloclemlo  7270  xrlttr  9549  fzen  9791  eluzgtdifelfzo  9942  ssfzo12bi  9970  climuni  11030  mulcn2  11049  serf0  11089  dfgcd2  11629  lcmgcdlem  11685  lcmdvds  11687  qnumdencl  11792  cnplimcim  12732  dveflem  12782
  Copyright terms: Public domain W3C validator