Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mp3an3an | Structured version Visualization version GIF version |
Description: mp3an 1452 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 1439 | . 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜂) |
6 | 1, 2, 5 | syl2an 595 | 1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: mp3an2ani 1459 unfilem2 8771 rankelun 9289 mul02 10806 fnn0ind 12069 supminf 12323 nn0p1elfzo 13068 faclbnd5 13646 pfxccatin12lem3 14082 mulre 14468 divalglem0 15732 algcvga 15911 infpn2 16237 prmgaplem7 16381 blssioo 23330 i1fsub 24236 itg1sub 24237 coesub 24774 dgrsub 24789 sincosq1eq 25025 logtayl2 25172 cxploglim 25482 uspgr2v1e2w 26960 ftc1anclem6 34853 |
Copyright terms: Public domain | W3C validator |