| 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 7414 marypha1lem 9473 wemaplem3 9588 xpwdomg 9625 pwfseqlem4 10702 wrdind 14760 wrd2ind 14761 sqrt2irr 16285 coprm 16748 oddprmdvds 16941 cyccom 19221 symggen 19488 efgredlemd 19762 efgredlem 19765 efgred 19766 chcoeffeq 22892 nmoleub2lem3 25148 iscmet3 25327 mulsproplem1 28142 axtgcgrid 28471 axtg5seg 28473 axtgbtwnid 28474 wlk1walk 29657 umgr2wlk 29969 frgrnbnb 30312 friendshipgt3 30417 ismntd 32974 archiexdiv 33197 fedgmullem2 33681 unelsiga 34135 sibfof 34342 bnj1145 35007 derangenlem 35176 irrdiff 37327 l1cvpat 39055 llnexchb2 39871 hdmapglem7 41931 eel11111 44743 dmrelrnrel 45231 climrec 45618 lptre2pt 45655 0ellimcdiv 45664 iccpartlt 47411 cycl3grtri 47914 |
| Copyright terms: Public domain | W3C validator |