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 586 | 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: fntp 6430 foimacnv 6667 respreima 6875 fpr 6958 fnprb 7013 curry1 7861 fnwelem 7887 frrlem12 8027 wfrlem13 8056 tfrlem10 8112 oawordeulem 8271 oelim2 8312 oaabs2 8363 omabs 8365 ssdomg 8663 limenpsi 8810 dffi2 9028 gruina 10415 recmulnq 10561 reclem2pr 10645 climeu 15099 cosmul 15715 2ebits 15987 algcvgblem 16115 ismgmid 18109 mndideu 18156 ga0 18664 efgs1 19097 distopon 21866 dfac14 22487 ptcmplem5 22925 sszcld 23686 itg11 24560 axlowdimlem13 27017 nbusgredgeu 27426 1trld 28197 cycpmconjslem1 31112 1stmbfm 31911 2ndmbfm 31912 bnj150 32541 f1resfz0f1d 32757 satfrel 33014 satf0n0 33025 bj-projval 34880 exidu1 35708 rngoideu 35755 rfcnpre1 42187 fundcmpsurinjlem2 44478 |
Copyright terms: Public domain | W3C validator |