![]() |
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 1206 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ w3a 1108 |
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 386 df-3an 1110 |
This theorem is referenced by: fresaunres1 6292 fvun2 6495 nnmsucr 7945 xrlttr 12220 iccdil 12564 icccntr 12566 absexpz 14386 posglbd 17465 f1omvdco3 18181 isdrngd 19090 unicld 21179 2ndcdisj2 21589 logrec 24845 cdj3lem3 29822 bnj563 31330 bnj1033 31554 stoweidlem14 40974 |
Copyright terms: Public domain | W3C validator |