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 218 | . 2 ⊢ (𝜑 → 𝜃) |
3 | syl3an3b.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl3an3 1161 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: fresaunres1 6551 fvun2 6755 nnmsucr 8251 xrlttr 12534 iccdil 12877 icccntr 12879 hashgt23el 13786 absexpz 14665 posglbd 17760 f1omvdco3 18577 isdrngd 19527 unicld 21654 2ndcdisj2 22065 logrec 25341 cdj3lem3 30215 bnj563 32014 bnj1033 32241 lindsadd 34900 nn0rppwr 39202 stoweidlem14 42319 |
Copyright terms: Public domain | W3C validator |