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  6744  nnaddcl  7715  nnmulcl  7716  zaddcllempos  8058  zaddcllemneg  8060  peano5uzti  8122  uzind2  8126  fzind  8129  zindd  8132  uzaddcl  8305  frec2uzltd  8870  iseqfveq2  8905  expivallem  8910  expcllem  8920  expap0  8939  mulexp  8948  expadd  8951  expmul  8954  leexp2r  8962  leexp1a  8963  bernneq  9022  cjexp  9121
  Copyright terms: Public domain W3C validator