|   | 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 582 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | 
| 5 | 1, 4 | sylan2br 595 | 1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ 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 207 df-an 396 | 
| This theorem is referenced by: sylancbr 601 reusv2 5402 rexopabb 5532 tz6.12 6930 r1ord3 9823 brdom7disj 10572 brdom6disj 10573 alephadd 10618 ltresr 11181 divmuldiv 11968 fnn0ind 12719 rexanuz 15385 nprmi 16727 lsmvalx 19658 cncfval 24915 angval 26845 amgmlem 27034 sspval 30743 sshjval 31370 sshjval3 31374 hosmval 31755 hodmval 31757 hfsmval 31758 opreu2reuALT 32497 broutsideof3 36128 mptsnunlem 37340 relowlpssretop 37366 line2ylem 48677 | 
| Copyright terms: Public domain | W3C validator |