![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl3an3b | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
Ref | Expression |
---|---|
syl3an3b.1 | ⊢ (𝜑 ↔ 𝜃) |
syl3an3b.2 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl3an3b | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an3b.1 | . . 3 ⊢ (𝜑 ↔ 𝜃) | |
2 | 1 | biimpi 208 | . 2 ⊢ (𝜑 → 𝜃) |
3 | syl3an3b.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl3an3 1211 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ w3a 1113 |
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 199 df-an 387 df-3an 1115 |
This theorem is referenced by: fresaunres1 6314 fvun2 6517 nnmsucr 7972 xrlttr 12259 iccdil 12603 icccntr 12605 absexpz 14422 posglbd 17503 f1omvdco3 18219 isdrngd 19128 unicld 21221 2ndcdisj2 21631 logrec 24903 cdj3lem3 29852 bnj563 31359 bnj1033 31583 lindsadd 33946 stoweidlem14 41025 |
Copyright terms: Public domain | W3C validator |