Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl6rbb | Structured version Visualization version GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6rbb.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
syl6rbb.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
syl6rbb | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6rbb.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | syl6rbb.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
3 | 1, 2 | syl6bb 288 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3 | bicomd 224 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: syl6rbbr 291 bibif 373 oranabs 993 necon4bid 3061 2reu4lem 4463 resopab2 5898 xpco 6134 funconstss 6819 xpopth 7721 snmapen 8579 ac6sfi 8751 supgtoreq 8923 rankr1bg 9221 alephsdom 9501 brdom7disj 9942 fpwwe2lem13 10053 nn0sub 11936 elznn0 11985 nn01to3 12330 supxrbnd1 12704 supxrbnd2 12705 rexuz3 14698 smueqlem 15829 qnumdenbi 16074 dfiso3 17033 lssne0 19653 pjfval2 20783 0top 21521 1stccn 22001 dscopn 23112 bcthlem1 23856 ovolgelb 24010 iblpos 24322 itgposval 24325 itgsubstlem 24574 sincosq3sgn 25015 sincosq4sgn 25016 lgsquadlem3 25886 colinearalg 26624 elntg2 26699 wlklnwwlkln2lem 27588 2pthdlem1 27637 wwlks2onsym 27665 rusgrnumwwlkb0 27678 numclwwlk2lem1 28083 nmoo0 28496 leop3 29830 leoptri 29841 f1od2 30384 tltnle 30577 fedgmullem2 30926 dfrdg4 33310 curf 34752 poimirlem28 34802 itgaddnclem2 34833 lfl1dim 36139 glbconxN 36396 2dim 36488 elpadd0 36827 dalawlem13 36901 diclspsn 38212 dihglb2 38360 dochsordN 38392 lzunuz 39245 uneqsn 40253 ntrclskb 40299 ntrneiel2 40316 infxrbnd2 41517 funressnfv 43159 funressndmafv2rn 43303 iccpartiltu 43429 |
Copyright terms: Public domain | W3C validator |