|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > sylbida | Structured version Visualization version GIF version | ||
| Description: A syllogism deduction. (Contributed by SN, 16-Jul-2024.) | 
| Ref | Expression | 
|---|---|
| sylbida.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | 
| sylbida.2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | 
| Ref | Expression | 
|---|---|
| sylbida | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | sylbida.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | biimpa 476 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | 
| 3 | sylbida.2 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
| 4 | 2, 3 | syldan 591 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 | 
| 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 | 
| This theorem is referenced by: fzdif1 13645 psdmul 22170 efrlim 27012 addsval 27995 mulscan2d 28205 dvdsruasso 33413 ssdifidlprm 33486 fsuppssind 42603 tfsconcat0i 43358 oadif1lem 43392 oadif1 43393 reabsifneg 43645 natglobalincr 46892 f1cof1b 47089 isubgr3stgrlem6 47938 prsthinc 49111 | 
| Copyright terms: Public domain | W3C validator |