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

Theorem adantld 267
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 107 . 2 ((𝜃𝜓) → 𝜓)
2 adantld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 32 1 (𝜑 → ((𝜃𝜓) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104
This theorem is referenced by:  jaoa  650  dedlema  887  dedlemb  888  prlem1  891  equveli  1658  poxp  5881  nnmordi  6120  eroprf  6230  xpdom2  6336  elni2  6470  prarloclemlo  6650  xrlttr  8817  fzen  9009  eluzgtdifelfzo  9155  ssfzo12bi  9183  climuni  10045  mulcn2  10064  serif0  10102
  Copyright terms: Public domain W3C validator