![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl5rbbr | Structured version Visualization version GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
syl5rbbr.1 | ⊢ (𝜓 ↔ 𝜑) |
syl5rbbr.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
syl5rbbr | ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5rbbr.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
2 | 1 | bicomi 214 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | syl5rbbr.2 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | syl5rbb 273 | 1 ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: sbco3 2445 necon2bbid 2866 fressnfv 6467 eluniima 6548 dfac2 8991 alephval2 9432 adderpqlem 9814 1idpr 9889 leloe 10162 negeq0 10373 muleqadd 10709 addltmul 11306 xrleloe 12015 fzrev 12441 mod0 12715 modirr 12781 cjne0 13947 lenegsq 14104 fsumsplit 14515 sumsplit 14543 dvdsabseq 15082 xpsfrnel 16270 isacs2 16361 acsfn 16367 comfeq 16413 sgrp2nmndlem3 17459 resscntz 17810 gexdvds 18045 hauscmplem 21257 hausdiag 21496 utop3cls 22102 ltgov 25537 ax5seglem4 25857 mdsl2i 29309 addeq0 29638 pl1cn 30129 topdifinfeq 33328 finxpreclem6 33363 ftc1anclem5 33619 fdc1 33672 relcnveq 34234 relcnveq2 34235 elrelscnveq 34382 elrelscnveq2 34383 lcvexchlem1 34639 lkreqN 34775 glbconxN 34982 islpln5 35139 islvol5 35183 cdlemefrs29bpre0 36001 cdlemg17h 36273 cdlemg33b 36312 brnonrel 38212 frege92 38566 e2ebind 39096 stoweidlem28 40563 |
Copyright terms: Public domain | W3C validator |