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 5570 oprabid 5865 nnmordi 6475 nnmord 6476 brecop 6582 findcard2 6846 findcard2s 6847 ordiso2 6991 zindd 9300 cau3lem 11042 climcau 11274 dvdsabseq 11770 metrest 13053 bj-charfunr 13533 |
Copyright terms: Public domain | W3C validator |