![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpdi | Structured version Visualization version GIF version |
Description: A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.) |
Ref | Expression |
---|---|
mpdi.1 | ⊢ (𝜓 → 𝜒) |
mpdi.2 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
mpdi | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpdi.1 | . . 3 ⊢ (𝜓 → 𝜒) | |
2 | 1 | a1i 11 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | mpdi.2 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
4 | 2, 3 | mpdd 43 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff setvar 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: mpii 46 pm2.43d 53 impt 178 sbcimdvOLD 3853 bropfvvvv 8078 wfrlem12OLD 8320 tfrlem9 8385 axcc2lem 10431 axdc3lem4 10448 fpwwe2lem7 10632 tskcard 10776 nqereu 10924 lbzbi 12920 fleqceilz 13819 ndvdsadd 16353 gcdneg 16463 ulmcaulem 25906 wlkiswwlks1 29121 elwspths2on 29214 relowlpssretop 36245 poimirlem18 36506 heicant 36523 brabg2 36585 neificl 36621 el1fzopredsuc 46033 |
Copyright terms: Public domain | W3C validator |