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  715  dedlema  964  dedlemb  965  prlem1  968  equveli  1752  poxp  6211  nnmordi  6495  eroprf  6606  xpdom2  6809  elni2  7276  prarloclemlo  7456  xrlttr  9752  fzen  9999  eluzgtdifelfzo  10153  ssfzo12bi  10181  climuni  11256  mulcn2  11275  serf0  11315  ntrivcvgap  11511  dfgcd2  11969  lcmgcdlem  12031  lcmdvds  12033  qnumdencl  12141  infpnlem1  12311  cnplimcim  13430  dveflem  13481  bj-charfundcALT  13844
  Copyright terms: Public domain W3C validator