| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sylanblrc | Structured version Visualization version GIF version | ||
| Description: Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.) |
| Ref | Expression |
|---|---|
| sylanblrc.1 | ⊢ (𝜑 → 𝜓) |
| sylanblrc.2 | ⊢ 𝜒 |
| sylanblrc.3 | ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒)) |
| Ref | Expression |
|---|---|
| sylanblrc | ⊢ (𝜑 → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sylanblrc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | sylanblrc.2 | . . 3 ⊢ 𝜒 | |
| 3 | 2 | a1i 11 | . 2 ⊢ (𝜑 → 𝜒) |
| 4 | sylanblrc.3 | . 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒)) | |
| 5 | 1, 3, 4 | sylanbrc 583 | 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: fntp 6627 foimacnv 6865 respreima 7086 fpr 7174 fnprb 7228 curry1 8129 fnwelem 8156 frrlem12 8322 wfrlem13OLD 8361 tfrlem10 8427 oawordeulem 8592 oelim2 8633 oaabs2 8687 omabs 8689 ssdomg 9040 limenpsi 9192 dffi2 9463 gruina 10858 recmulnq 11004 reclem2pr 11088 climeu 15591 cosmul 16209 2ebits 16484 algcvgblem 16614 ismgmid 18678 mndideu 18758 ga0 19316 efgs1 19753 pzriprnglem4 21495 psdmvr 22173 distopon 23004 dfac14 23626 ptcmplem5 24064 sszcld 24839 itg11 25726 axlowdimlem13 28969 nbusgredgeu 29383 1trld 30161 s1chn 33000 cycpmconjslem1 33174 1stmbfm 34262 2ndmbfm 34263 bnj150 34890 f1resfz0f1d 35119 satfrel 35372 satf0n0 35383 bj-projval 36997 exidu1 37863 rngoideu 37910 refrelressn 38525 rfcnpre1 45024 fundcmpsurinjlem2 47386 |
| Copyright terms: Public domain | W3C validator |