![]() |
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 7397 marypha1lem 9448 wemaplem3 9563 xpwdomg 9600 wrdind 14696 wrd2ind 14697 sqrt2irr 16217 coprm 16673 oddprmdvds 16863 cyccom 19149 symggen 19416 efgredlemd 19690 efgredlem 19693 efgred 19694 chcoeffeq 22775 nmoleub2lem3 25029 iscmet3 25208 mulsproplem1 28003 axtgcgrid 28254 axtg5seg 28256 axtgbtwnid 28257 wlk1walk 29440 umgr2wlk 29747 frgrnbnb 30090 friendshipgt3 30195 ismntd 32693 archiexdiv 32876 fedgmullem2 33260 unelsiga 33689 sibfof 33896 bnj1145 34560 derangenlem 34717 irrdiff 36741 l1cvpat 38463 llnexchb2 39279 hdmapglem7 41339 eel11111 44085 dmrelrnrel 44522 climrec 44914 lptre2pt 44951 0ellimcdiv 44960 iccpartlt 46687 |
Copyright terms: Public domain | W3C validator |