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  709  dedlema  953  dedlemb  954  prlem1  957  equveli  1732  poxp  6122  nnmordi  6405  eroprf  6515  xpdom2  6718  elni2  7115  prarloclemlo  7295  xrlttr  9574  fzen  9816  eluzgtdifelfzo  9967  ssfzo12bi  9995  climuni  11055  mulcn2  11074  serf0  11114  ntrivcvgap  11310  dfgcd2  11691  lcmgcdlem  11747  lcmdvds  11749  qnumdencl  11854  cnplimcim  12794  dveflem  12844
  Copyright terms: Public domain W3C validator