Theorem sylbbr 228

Description: A mixed syllogism inference from two biconditionals.

Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 17 infers an implication from two implications (and there are 3syl 18 and 4syl 19 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 209, sylib 210, sylbir 227, sylibr 226; four inferences inferring an implication from two biconditionals: sylbb 211, sylbbr 228, sylbb1 229, sylbb2 230; four inferences inferring a biconditional from two biconditionals: bitri 267, bitr2i 268, bitr3i 269, bitr4i 270 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 47, syl5 34, syl6 35, mpbid 224, bitrd 271, syl5bb 275, syl6bb 279 and variants. (Contributed by BJ, 21-Apr-2019.)

Hypotheses

Ref	Expression
sylbbr.1	⊢ (𝜑 ↔ 𝜓)
sylbbr.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
sylbbr	⊢ (𝜒 → 𝜑)

Proof of Theorem sylbbr

Step	Hyp	Ref	Expression
1		sylbbr.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
2	1	biimpri 220	. 2 ⊢ (𝜒 → 𝜓)
3		sylbbr.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	sylibr 226	1 ⊢ (𝜒 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  bitri  267  euelss  4114  dfnfc2  4648  ndmima  5719  axcclem  9567  fsumcom2  14844  fprodcom2  15051  pmtr3ncomlem1  18205  mdetunilem7  20750  cmpcov2  21522  umgredg  26374  vtxdginducedm1  26793  2pthfrgrrn  27631  conway  32423  f1omptsnlem  33682  igenval2  34352  mpt2bi123f  34457  brtrclfv2  38802  clsk1indlem3  39123