![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylanbr | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
sylanbr.1 | ⊢ (𝜓 ↔ 𝜑) |
sylanbr.2 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
sylanbr | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylanbr.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
2 | 1 | biimpri 218 | . 2 ⊢ (𝜑 → 𝜓) |
3 | sylanbr.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 569 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: syl2anbr 586 funfv 6407 2mpt20 7029 tfrlem7 7632 omword 7804 isinf 8329 fsuppunbi 8452 axdc3lem2 9475 supsrlem 10134 expclzlem 13091 expgt0 13100 expge0 13103 expge1 13104 swrdnd2 13642 resqrex 14199 rplpwr 15484 4sqlem19 15874 gexcl3 18209 thlle 20258 decpmataa0 20793 neindisj 21142 ptcmplem5 22080 tsmsxplem1 22176 tsmsxplem2 22177 elovolmr 23464 itgsubst 24032 logeftb 24551 logbchbase 24730 legov 25701 unopbd 29214 nmcoplb 29229 nmcfnlb 29253 nmopcoi 29294 iocinif 29883 voliune 30632 signstfvneq0 30989 nosupbnd1lem5 32195 f1omptsnlem 33520 unccur 33725 matunitlindflem2 33739 stoweidlem15 40749 hoiqssbllem3 41358 vonioo 41416 vonicc 41419 gboge9 42180 |
Copyright terms: Public domain | W3C validator |