![]() |
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 1156 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) |
5 | syl3anb.4 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) | |
6 | 4, 5 | sylbi 216 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: syl3anbr 1163 poxp 8114 infempty 9502 symgsssg 19335 symgfisg 19336 lmodvscl 20489 xrs1mnd 20983 iscnp2 22743 clwwlknccat 29316 slmdvscl 32359 cgr3permute3 35019 cgr3permute1 35020 cgr3permute2 35021 cgr3permute4 35022 cgr3permute5 35023 colinearxfr 35047 grposnOLD 36750 rngunsnply 41915 |
Copyright terms: Public domain | W3C validator |