![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > a2d | GIF version |
Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.) |
Ref | Expression |
---|---|
a2d.1 | ⊢ (φ → (ψ → (χ → θ))) |
Ref | Expression |
---|---|
a2d | ⊢ (φ → ((ψ → χ) → (ψ → θ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a2d.1 | . 2 ⊢ (φ → (ψ → (χ → θ))) | |
2 | ax-2 6 | . 2 ⊢ ((ψ → (χ → θ)) → ((ψ → χ) → (ψ → θ))) | |
3 | 1, 2 | syl 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 |