ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantld GIF 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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
adantld (𝜑 → ((𝜃𝜓) → 𝜒))

Proof of Theorem adantld
StepHypRef Expression
1 simpr 108 . 2 ((𝜃𝜓) → 𝜓)
2 adantld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 32 1 (𝜑 → ((𝜃𝜓) → 𝜒))
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  913  dedlemb  914  prlem1  917  equveli  1686  poxp  5954  nnmordi  6227  eroprf  6337  xpdom2  6499  elni2  6817  prarloclemlo  6997  xrlttr  9197  fzen  9389  eluzgtdifelfzo  9536  ssfzo12bi  9564  climuni  10576  mulcn2  10595  serif0  10633  dfgcd2  10885  lcmgcdlem  10941  lcmdvds  10943  qnumdencl  11047
  Copyright terms: Public domain W3C validator