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

Theorem a2d 23
Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)
Hypothesis
Ref Expression
a2d.1 (φ → (ψ → (χθ)))
Assertion
Ref Expression
a2d (φ → ((ψχ) → (ψθ)))

Proof of Theorem a2d
StepHypRef Expression
1 a2d.1 . 2 (φ → (ψ → (χθ)))
2 ax-2 6 . 2 ((ψ → (χθ)) → ((ψχ) → (ψθ)))
31, 2syl 14 1 (φ → ((ψχ) → (ψθ)))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  mpdd  36  imim2d  48  imim3i  55  loowoz  96  cbv1  1614  ralimdaa  2364  reuss2  3194  finds2  4251  ssrel  4355  ssrel2  4357  ssrelrel  4367  funfvima2  5316  tfrlem1  5845  tfrlemi1  5867  tfri3  5875  rdgon  5893
  Copyright terms: Public domain W3C validator