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 18 infers an implication from two implications (and there are 3syl 19 and 4syl 20 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 48, syl5 35, syl6 36, mpbid 235, bitrd 282, bitrid 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 ⊢ (𝜒 → 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bitri  278  euelss  4284  dfnfc2  4893  ndmima  6104  unfi  9153  axcclem  10447  cshw1  14866  fsumcom2  15832  fprodcom2  16045  pmtr3ncomlem1  19549  rspprop  21381  mdetunilem7  22786  cmpcov2  23558  hausflf2  24166  conway  27983  umgredg  29499  vtxdginducedm1  29904  2pthfrgrrn  30644  eqdif  32876  padct  33074  cusgredgex2  35623  f1omptsnlem  38010  igenval2  38745  mpobi123f  38839  dmqsblocks  39644  brtrclfv2  44481  clsk1indlem3  44797  permaxpow  45746  permaxpr  45747  or2expropbilem1  47797  grtriproplem  48732  mo0sn  49622