| 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 228 | . 2 ⊢ (𝜑 → 𝜓) |
| 3 | sylanbr.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
| 4 | 2, 3 | sylan 580 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: syl2anbr 599 rspc4v 3642 funfv 6996 2mpo0 7682 tfrlem7 8423 omword 8608 isinf 9296 isinfOLD 9297 fsuppunbi 9429 axdc3lem2 10491 supsrlem 11151 expclzlem 14124 expgt0 14136 expge0 14139 expge1 14140 swrdnd2 14693 resqrex 15289 rplpwr 16595 4sqlem19 17001 gexcl3 19605 thlle 21716 thlleOLD 21717 decpmataa0 22774 neindisj 23125 ptcmplem5 24064 tsmsxplem1 24161 tsmsxplem2 24162 elovolmr 25511 itgsubst 26090 logeftb 26625 logbchbase 26814 nosupbnd1lem5 27757 noinfbnd1lem5 27772 legov 28593 unopbd 32034 nmcoplb 32049 nmcfnlb 32073 nmopcoi 32114 an52ds 32470 an62ds 32471 an72ds 32472 an82ds 32473 iocinif 32783 1arithufdlem4 33575 r1plmhm 33630 r1pquslmic 33631 voliune 34230 signstfvneq0 34587 lfuhgr3 35125 f1omptsnlem 37337 unccur 37610 matunitlindflem2 37624 stoweidlem15 46030 hoiqssbllem3 46639 vonioo 46697 vonicc 46700 gboge9 47751 catprs 48900 |
| Copyright terms: Public domain | W3C validator |