![]() |
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 220 | . 2 ⊢ (𝜑 → 𝜓) |
3 | sylanbr.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 575 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 |
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 387 |
This theorem is referenced by: syl2anbr 592 funfv 6525 2mpt20 7159 tfrlem7 7762 omword 7934 isinf 8461 fsuppunbi 8584 axdc3lem2 9608 supsrlem 10268 expclzlem 13202 expgt0 13211 expge0 13214 expge1 13215 swrdnd2 13750 resqrex 14398 rplpwr 15682 4sqlem19 16071 gexcl3 18386 thlle 20440 decpmataa0 20980 neindisj 21329 ptcmplem5 22268 tsmsxplem1 22364 tsmsxplem2 22365 elovolmr 23680 itgsubst 24249 logeftb 24767 logbchbase 24949 legov 25936 unopbd 29446 nmcoplb 29461 nmcfnlb 29485 nmopcoi 29526 iocinif 30107 voliune 30890 signstfvneq0 31250 nosupbnd1lem5 32447 f1omptsnlem 33779 unccur 34019 matunitlindflem2 34034 stoweidlem15 41163 hoiqssbllem3 41769 vonioo 41827 vonicc 41830 gboge9 42681 |
Copyright terms: Public domain | W3C validator |