![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mp2d | Structured version Visualization version GIF version |
Description: A double modus ponens deduction. Deduction associated with mp2 9. (Contributed by NM, 23-May-2013.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
Ref | Expression |
---|---|
mp2d.1 | ⊢ (𝜑 → 𝜓) |
mp2d.2 | ⊢ (𝜑 → 𝜒) |
mp2d.3 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
mp2d | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp2d.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | mp2d.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | mp2d.3 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
4 | 2, 3 | mpid 44 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 1, 4 | mpd 15 | 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: riotaeqimp 7399 marypha1lem 9469 wemaplem3 9584 xpwdomg 9621 wrdind 14725 wrd2ind 14726 sqrt2irr 16246 coprm 16707 oddprmdvds 16900 cyccom 19193 symggen 19464 efgredlemd 19738 efgredlem 19741 efgred 19742 chcoeffeq 22876 nmoleub2lem3 25130 iscmet3 25309 mulsproplem1 28114 axtgcgrid 28387 axtg5seg 28389 axtgbtwnid 28390 wlk1walk 29573 umgr2wlk 29880 frgrnbnb 30223 friendshipgt3 30328 ismntd 32857 archiexdiv 33059 fedgmullem2 33531 unelsiga 33980 sibfof 34187 bnj1145 34851 derangenlem 35012 irrdiff 37046 l1cvpat 38765 llnexchb2 39581 hdmapglem7 41641 eel11111 44436 dmrelrnrel 44869 climrec 45260 lptre2pt 45297 0ellimcdiv 45306 iccpartlt 47032 |
Copyright terms: Public domain | W3C validator |