Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl2anbr | Structured version Visualization version GIF version |
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |
Ref | Expression |
---|---|
syl2anbr.1 | ⊢ (𝜓 ↔ 𝜑) |
syl2anbr.2 | ⊢ (𝜒 ↔ 𝜏) |
syl2anbr.3 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
syl2anbr | ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2anbr.2 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
2 | syl2anbr.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
3 | syl2anbr.3 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylanbr 585 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2br 598 | 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: sylancbr 604 reusv2 5305 rexopabb 5418 tz6.12 6749 r1ord3 9411 brdom7disj 10158 brdom6disj 10159 alephadd 10204 ltresr 10767 divmuldiv 11545 fnn0ind 12289 rexanuz 14922 nprmi 16259 lsmvalx 19041 cncfval 23798 angval 25697 amgmlem 25885 sspval 28817 sshjval 29444 sshjval3 29448 hosmval 29829 hodmval 29831 hfsmval 29832 opreu2reuALT 30557 broutsideof3 34178 mptsnunlem 35259 relowlpssretop 35285 line2ylem 45785 |
Copyright terms: Public domain | W3C validator |