|   | 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 1155 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) | 
| 5 | syl3anb.4 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) | |
| 6 | 4, 5 | sylbi 217 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1086 | 
| 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 df-3an 1088 | 
| This theorem is referenced by: syl3anbr 1162 poxp 8154 infempty 9548 symgsssg 19486 symgfisg 19487 lmodvscl 20877 xrs1mnd 21423 iscnp2 23248 clwwlknccat 30083 slmdvscl 33221 cgr3permute3 36049 cgr3permute1 36050 cgr3permute2 36051 cgr3permute4 36052 cgr3permute5 36053 colinearxfr 36077 grposnOLD 37890 rngunsnply 43186 | 
| Copyright terms: Public domain | W3C validator |