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 231 | . 2 ⊢ (𝜑 → 𝜓) |
3 | sylanbr.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 583 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: syl2anbr 602 funfv 6820 2mpo0 7476 tfrlem7 8143 omword 8322 isinf 8921 fsuppunbi 9036 axdc3lem2 10095 supsrlem 10755 expclzlem 13691 expgt0 13701 expge0 13704 expge1 13705 swrdnd2 14253 resqrex 14847 rplpwr 16152 4sqlem19 16549 gexcl3 19009 thlle 20692 decpmataa0 21697 neindisj 22046 ptcmplem5 22985 tsmsxplem1 23082 tsmsxplem2 23083 elovolmr 24405 itgsubst 24978 logeftb 25504 logbchbase 25686 legov 26708 unopbd 30128 nmcoplb 30143 nmcfnlb 30167 nmopcoi 30208 iocinif 30854 voliune 31941 signstfvneq0 32295 lfuhgr3 32825 nosupbnd1lem5 33686 noinfbnd1lem5 33701 f1omptsnlem 35281 unccur 35534 matunitlindflem2 35548 stoweidlem15 43277 hoiqssbllem3 43883 vonioo 43941 vonicc 43944 gboge9 44935 catprs 46011 |
Copyright terms: Public domain | W3C validator |