![]() |
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 215 | . 2 ⊢ (𝜑 → 𝜃) |
3 | syl3an3b.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl3an3 1162 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: fnunres2 6668 fresaunres1 6770 fvun2 6989 fvpr2g 7200 nnmsucr 8646 entrfil 9213 enpr2 10027 xrlttr 13154 iccdil 13502 icccntr 13504 hashgt23el 14419 absexpz 15288 posglbdg 18410 f1omvdco3 19416 isdrngd 20669 isdrngdOLD 20671 unicld 22994 2ndcdisj2 23405 logrec 26740 cdj3lem3 32320 bnj563 34505 bnj1033 34731 lindsadd 37217 nn0rppwr 42028 stoweidlem14 45540 |
Copyright terms: Public domain | W3C validator |