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  1629  ralimdaa  2380  reuss2  3211  finds2  4267  ssrel  4371  ssrel2  4373  ssrelrel  4383  funfvima2  5334  tfrlem1  5864  tfrlemi1  5887  tfri3  5894  rdgon  5913  pitonn  6704  nnaddcl  7675  nnmulcl  7676  zaddcllempos  8018  zaddcllemneg  8020  peano5uzti  8082  uzind2  8086  fzind  8089  zindd  8092  uzaddcl  8265  frec2uzltd  8830  iseqfveq2  8865  expivallem  8870  expcllem  8880  expap0  8899  mulexp  8908  expadd  8911  expmul  8914  leexp2r  8922  leexp1a  8923  bernneq  8982  cjexp  9081
  Copyright terms: Public domain W3C validator