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 1369 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 514 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl1111anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl1111anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl1111anc.5 | . 2 ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂) | |
7 | 3, 4, 5, 6 | syl21anc 835 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: mpsyl4anc 838 ucnima 22885 f1otrge 26656 swrdf1 30630 cycpmrn 30806 linds2eq 30963 idlmulssprm 30982 isprmidlc 30987 prmidlc 30988 qsidomlem2 30990 lbsdiflsp0 31046 extdg1id 31077 3cubeslem1 39357 sineq0ALT 41345 cncfshift 42231 cncfperiod 42236 |
Copyright terms: Public domain | W3C validator |