![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl3anb | Structured version Visualization version GIF version |
Description: A triple syllogism inference. (Contributed by NM, 15-Oct-2005.) |
Ref | Expression |
---|---|
syl3anb.1 | ⊢ (𝜑 ↔ 𝜓) |
syl3anb.2 | ⊢ (𝜒 ↔ 𝜃) |
syl3anb.3 | ⊢ (𝜏 ↔ 𝜂) |
syl3anb.4 | ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) |
Ref | Expression |
---|---|
syl3anb | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anb.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | syl3anb.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
3 | syl3anb.3 | . . 3 ⊢ (𝜏 ↔ 𝜂) | |
4 | 1, 2, 3 | 3anbi123i 1152 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) |
5 | syl3anb.4 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) | |
6 | 4, 5 | sylbi 216 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1084 |
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 396 df-3an 1086 |
This theorem is referenced by: syl3anbr 1159 poxp 8108 infempty 9497 symgsssg 19372 symgfisg 19373 lmodvscl 20709 xrs1mnd 21262 iscnp2 23053 clwwlknccat 29740 slmdvscl 32786 cgr3permute3 35480 cgr3permute1 35481 cgr3permute2 35482 cgr3permute4 35483 cgr3permute5 35484 colinearxfr 35508 grposnOLD 37206 rngunsnply 42370 |
Copyright terms: Public domain | W3C validator |