![]() |
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 577 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2br 588 | 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: sylancbr 594 reusv2 5105 tz6.12 6460 r1ord3 8929 brdom7disj 9675 brdom6disj 9676 alephadd 9721 ltresr 10284 divmuldiv 11058 fnn0ind 11811 rexanuz 14469 nprmi 15781 lsmvalx 18412 cncfval 23068 angval 24948 amgmlem 25136 sspval 28129 sshjval 28760 sshjval3 28764 hosmval 29145 hodmval 29147 hfsmval 29148 broutsideof3 32767 mptsnunlem 33730 relowlpssretop 33756 line2ylem 43317 |
Copyright terms: Public domain | W3C validator |