Theorem sylbbr 238

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 219, sylib 220, sylbir 237, sylibr 236; four inferences inferring an implication from two biconditionals: sylbb 221, sylbbr 238, sylbb1 239, sylbb2 240; four inferences inferring a biconditional from two biconditionals: bitri 277, bitr2i 278, bitr3i 279, bitr4i 280 (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 234, bitrd 281, syl5bb 285, syl6bb 289 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 230	. 2 ⊢ (𝜒 → 𝜓)
3		sylbbr.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	sylibr 236	1 ⊢ (𝜒 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitri  277  euelss  4278  dfnfc2  4846  ndmima  5952  axcclem  9865  cshw1  14169  fsumcom2  15114  fprodcom2  15323  pmtr3ncomlem1  18584  mdetunilem7  21210  cmpcov2  21981  hausflf2  22589  umgredg  26909  vtxdginducedm1  27311  2pthfrgrrn  28045  eqdif  30267  cusgredgex2  32376  conway  33271  f1omptsnlem  34633  igenval2  35376  mpobi123f  35472  brtrclfv2  40162  clsk1indlem3  40483  or2expropbilem1  43357