| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl1111anc | Structured version Visualization version GIF version | ||
| Description: Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1376 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.) |
| Ref | Expression |
|---|---|
| syl1111anc.1 | ⊢ (𝜑 → 𝜓) |
| syl1111anc.2 | ⊢ (𝜑 → 𝜒) |
| syl1111anc.3 | ⊢ (𝜑 → 𝜃) |
| syl1111anc.4 | ⊢ (𝜑 → 𝜏) |
| syl1111anc.5 | ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂) |
| Ref | Expression |
|---|---|
| syl1111anc | ⊢ (𝜑 → 𝜂) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl1111anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | syl1111anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
| 3 | 1, 2 | jca 511 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
| 4 | syl1111anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
| 5 | syl1111anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
| 6 | syl1111anc.5 | . 2 ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂) | |
| 7 | 3, 4, 5, 6 | syl21anc 838 | 1 ⊢ (𝜑 → 𝜂) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 |
| This theorem is referenced by: mpsyl4anc 843 ucnima 24290 f1otrge 28880 swrdf1 32941 mgcf1o 32993 chnind 33001 gsumfs2d 33058 cycpmrn 33163 linds2eq 33409 rhmimaidl 33460 idlmulssprm 33470 isprmidlc 33475 prmidlc 33476 qsidomlem2 33481 ply1unit 33600 lbsdiflsp0 33677 extdg1id 33716 3cubeslem1 42695 cantnftermord 43333 sineq0ALT 44957 cncfshift 45889 cncfperiod 45894 |
| Copyright terms: Public domain | W3C validator |