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 205 | . 2 ⊢ (𝜑 → 𝜃) |
3 | syl3an3b.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl3an3 1353 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: fresaunres1 5990 fvun2 6180 nnmsucr 7592 xrlttr 11849 iccdil 12181 icccntr 12183 absexpz 13893 posglbd 16973 f1omvdco3 17692 isdrngd 18595 unicld 20660 2ndcdisj2 21070 logrec 24301 cdj3lem3 28681 bnj563 30067 bnj1033 30291 stoweidlem14 38907 |
Copyright terms: Public domain | W3C validator |