![]() |
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 13642 psdmul 22188 efrlim 27027 addsval 28010 mulscan2d 28220 dvdsruasso 33393 ssdifidlprm 33466 fsuppssind 42580 tfsconcat0i 43335 oadif1lem 43369 oadif1 43370 reabsifneg 43622 natglobalincr 46831 f1cof1b 47027 isubgr3stgrlem6 47874 prsthinc 48855 |
Copyright terms: Public domain | W3C validator |