Theorem sylbbr 239

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 220, sylib 221, sylbir 238, sylibr 237; four inferences inferring an implication from two biconditionals: sylbb 222, sylbbr 239, sylbb1 240, sylbb2 241; four inferences inferring a biconditional from two biconditionals: bitri 278, bitr2i 279, bitr3i 280, bitr4i 281 (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 235, bitrd 282, syl5bb 286, bitrdi 290 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 231	. 2 ⊢ (𝜒 → 𝜓)
3		sylbbr.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	sylibr 237	1 ⊢ (𝜒 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitri  278  euelss  4224  dfnfc2  4822  ndmima  5938  unfi  8741  axcclem  9917  cshw1  14231  fsumcom2  15177  fprodcom2  15386  pmtr3ncomlem1  18668  mdetunilem7  21318  cmpcov2  22090  hausflf2  22698  umgredg  27030  vtxdginducedm1  27432  2pthfrgrrn  28166  eqdif  30388  cusgredgex2  32600  conway  33556  f1omptsnlem  35033  igenval2  35784  mpobi123f  35880  brtrclfv2  40801  clsk1indlem3  41119  or2expropbilem1  43990