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

Theorem adantld 273
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-1 5  ax-2 6  ax-mp 7  ax-ia2 106
This theorem is referenced by:  jaoa  676  dedlema  916  dedlemb  917  prlem1  920  equveli  1690  poxp  6011  nnmordi  6289  eroprf  6399  xpdom2  6601  elni2  6927  prarloclemlo  7107  xrlttr  9319  fzen  9511  eluzgtdifelfzo  9662  ssfzo12bi  9690  climuni  10735  mulcn2  10755  serf0  10795  dfgcd2  11335  lcmgcdlem  11391  lcmdvds  11393  qnumdencl  11497
  Copyright terms: Public domain W3C validator