Theorem sylbbr 226

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 207, sylib 208, sylbir 225, sylibr 224; four inferences inferring an implication from two biconditionals: sylbb 209, sylbbr 226, sylbb1 227, sylbb2 228; four inferences inferring a biconditional from two biconditionals: bitri 264, bitr2i 265, bitr3i 266, bitr4i 267 (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 222, bitrd 268, syl5bb 272, syl6bb 276 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 218	. 2 ⊢ (𝜒 → 𝜓)
3		sylbbr.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	sylibr 224	1 ⊢ (𝜒 → 𝜑)

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:  bitri  264  euelss  3914  dfnfc2  4454  ndmima  5502  axcclem  9279  fsumcom2  14505  fprodcom2  14714  pmtr3ncomlem1  17893  mdetunilem7  20424  cmpcov2  21193  umgredg  26033  vtxdginducedm1  26439  clwwlksnndef  26890  2pthfrgrrn  27146  conway  31910  f1omptsnlem  33183  igenval2  33865  mpt2bi123f  33971  brtrclfv2  38019  clsk1indlem3  38341