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 1147 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) |
5 | syl3anb.4 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) | |
6 | 4, 5 | sylbi 218 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: syl3anbr 1154 poxp 7811 infempty 8959 symgsssg 18524 symgfisg 18525 lmodvscl 19580 xrs1mnd 20511 iscnp2 21775 clwwlknccat 27769 slmdvscl 30769 cgr3permute3 33405 cgr3permute1 33406 cgr3permute2 33407 cgr3permute4 33408 cgr3permute5 33409 colinearxfr 33433 grposnOLD 35041 rngunsnply 39651 |
Copyright terms: Public domain | W3C validator |