![]() |
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 1373 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 842 ucnima 24306 f1otrge 28895 swrdf1 32926 mgcf1o 32978 chnind 32985 gsumfs2d 33041 cycpmrn 33146 linds2eq 33389 rhmimaidl 33440 idlmulssprm 33450 isprmidlc 33455 prmidlc 33456 qsidomlem2 33461 ply1unit 33580 lbsdiflsp0 33654 extdg1id 33691 3cubeslem1 42672 cantnftermord 43310 sineq0ALT 44935 cncfshift 45830 cncfperiod 45835 |
Copyright terms: Public domain | W3C validator |