| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mp3an3an | Structured version Visualization version GIF version | ||
| Description: mp3an 1463 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
| Ref | Expression |
|---|---|
| mp3an3an.1 | ⊢ 𝜑 |
| mp3an3an.2 | ⊢ (𝜓 → 𝜒) |
| mp3an3an.3 | ⊢ (𝜃 → 𝜏) |
| mp3an3an.4 | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) |
| Ref | Expression |
|---|---|
| mp3an3an | ⊢ ((𝜓 ∧ 𝜃) → 𝜂) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mp3an3an.2 | . 2 ⊢ (𝜓 → 𝜒) | |
| 2 | mp3an3an.3 | . 2 ⊢ (𝜃 → 𝜏) | |
| 3 | mp3an3an.1 | . . 3 ⊢ 𝜑 | |
| 4 | mp3an3an.4 | . . 3 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) | |
| 5 | 3, 4 | mp3an1 1450 | . 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜂) |
| 6 | 1, 2, 5 | syl2an 596 | 1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: mp3an2ani 1470 unfilem2 9344 rankelun 9912 mul02 11439 fnn0ind 12717 supminf 12977 nn0p1elfzo 13742 faclbnd5 14337 pfxccatin12lem3 14770 mulre 15160 divalglem0 16430 algcvga 16616 infpn2 16951 prmgaplem7 17095 blssioo 24816 i1fsub 25743 itg1sub 25744 coesub 26296 dgrsub 26312 sincosq1eq 26554 logtayl2 26704 cxploglim 27021 uspgr2v1e2w 29268 ftc1anclem6 37705 plusmod5ne 47347 io1ii 48818 |
| Copyright terms: Public domain | W3C validator |