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

Theorem adantld 278
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 110 . 2 ((𝜃𝜓) → 𝜓)
2 adantld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 32 1 (𝜑 → ((𝜃𝜓) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107
This theorem is referenced by:  jaoa  721  dedlema  971  dedlemb  972  prlem1  975  equveli  1770  poxp  6258  nnmordi  6542  eroprf  6655  xpdom2  6858  elni2  7344  prarloclemlo  7524  xrlttr  9827  fzen  10075  eluzgtdifelfzo  10229  ssfzo12bi  10257  climuni  11336  mulcn2  11355  serf0  11395  ntrivcvgap  11591  dfgcd2  12050  lcmgcdlem  12112  lcmdvds  12114  qnumdencl  12222  infpnlem1  12394  cnplimcim  14613  dveflem  14664  bj-charfundcALT  15039
  Copyright terms: Public domain W3C validator