![]() |
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 1374 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 512 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl1111anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl1111anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl1111anc.5 | . 2 ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂) | |
7 | 3, 4, 5, 6 | syl21anc 836 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: mpsyl4anc 840 ucnima 23793 f1otrge 28161 swrdf1 32158 mgcf1o 32211 cycpmrn 32343 linds2eq 32542 rhmimaidl 32595 idlmulssprm 32605 isprmidlc 32611 prmidlc 32612 qsidomlem2 32617 lbsdiflsp0 32770 extdg1id 32801 3cubeslem1 41504 cantnftermord 42152 sineq0ALT 43780 cncfshift 44669 cncfperiod 44674 |
Copyright terms: Public domain | W3C validator |