![]() |
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 3812 bropfvvvv 8016 wfrlem12OLD 8258 tfrlem9 8323 axcc2lem 10330 axdc3lem4 10347 fpwwe2lem7 10531 tskcard 10675 nqereu 10823 lbzbi 12815 fleqceilz 13713 ndvdsadd 16251 gcdneg 16361 ulmcaulem 25704 wlkiswwlks1 28640 elwspths2on 28733 relowlpssretop 35766 poimirlem18 36027 heicant 36044 brabg2 36106 neificl 36143 el1fzopredsuc 45451 |
Copyright terms: Public domain | W3C validator |