Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpdd | GIF version |
Description: A nested modus ponens deduction. (Contributed by NM, 12-Dec-2004.) |
Ref | Expression |
---|---|
mpdd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
mpdd.2 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
mpdd | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpdd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | mpdd.2 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
3 | 2 | a2d 26 | . 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃))) |
4 | 1, 3 | mpd 13 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: mpid 42 mpdi 43 syld 45 syl6c 66 mpteqb 5511 oprabid 5803 nnmordi 6412 nnmord 6413 brecop 6519 findcard2 6783 findcard2s 6784 ordiso2 6920 zindd 9169 cau3lem 10886 climcau 11116 dvdsabseq 11545 metrest 12675 |
Copyright terms: Public domain | W3C validator |