![]() |
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 581 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2br 594 | 1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 396 |
This theorem is referenced by: sylancbr 600 reusv2 5391 rexopabb 5518 tz6.12 6906 r1ord3 9772 brdom7disj 10521 brdom6disj 10522 alephadd 10567 ltresr 11130 divmuldiv 11910 fnn0ind 12657 rexanuz 15288 nprmi 16622 lsmvalx 19544 cncfval 24718 angval 26637 amgmlem 26826 sspval 30400 sshjval 31027 sshjval3 31031 hosmval 31412 hodmval 31414 hfsmval 31415 opreu2reuALT 32141 broutsideof3 35559 mptsnunlem 36675 relowlpssretop 36701 line2ylem 47591 |
Copyright terms: Public domain | W3C validator |