![]() |
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 227 | . 2 ⊢ (𝜑 → 𝜓) |
3 | sylanbr.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 578 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 |
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 |
This theorem is referenced by: syl2anbr 597 rspc4v 3626 funfv 6981 2mpo0 7667 tfrlem7 8405 omword 8592 isinf 9287 isinfOLD 9288 fsuppunbi 9425 axdc3lem2 10485 supsrlem 11145 expclzlem 14097 expgt0 14109 expge0 14112 expge1 14113 swrdnd2 14658 resqrex 15250 rplpwr 16554 4sqlem19 16960 gexcl3 19581 thlle 21690 thlleOLD 21691 decpmataa0 22758 neindisj 23109 ptcmplem5 24048 tsmsxplem1 24145 tsmsxplem2 24146 elovolmr 25493 itgsubst 26072 logeftb 26607 logbchbase 26796 nosupbnd1lem5 27739 noinfbnd1lem5 27754 legov 28509 unopbd 31945 nmcoplb 31960 nmcfnlb 31984 nmopcoi 32025 an52ds 32378 an62ds 32379 an72ds 32380 an82ds 32381 iocinif 32686 1arithufdlem4 33428 r1plmhm 33483 r1pquslmic 33484 voliune 34075 signstfvneq0 34431 lfuhgr3 34960 f1omptsnlem 37056 unccur 37317 matunitlindflem2 37331 stoweidlem15 45672 hoiqssbllem3 46281 vonioo 46339 vonicc 46342 gboge9 47372 catprs 48368 |
Copyright terms: Public domain | W3C validator |