Theorem sylbbr 236

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 217, sylib 218, sylbir 235, sylibr 234; four inferences inferring an implication from two biconditionals: sylbb 219, sylbbr 236, sylbb1 237, sylbb2 238; four inferences inferring a biconditional from two biconditionals: bitri 275, bitr2i 276, bitr3i 277, bitr4i 278 (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 232, bitrd 279, bitrid 283, bitrdi 287 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 228	. 2 ⊢ (𝜒 → 𝜓)
3		sylbbr.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	sylibr 234	1 ⊢ (𝜒 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bitri  275  euelss  4286  dfnfc2  4887  ndmima  6072  unfi  9109  axcclem  10381  cshw1  14759  fsumcom2  15711  fprodcom2  15921  pmtr3ncomlem1  19419  mdetunilem7  22579  cmpcov2  23351  hausflf2  23959  conway  27792  umgredg  29229  vtxdginducedm1  29635  2pthfrgrrn  30375  eqdif  32612  padct  32814  cusgredgex2  35345  f1omptsnlem  37618  igenval2  38346  mpobi123f  38442  dmqsblocks  39247  brtrclfv2  44112  clsk1indlem3  44428  permaxpow  45394  permaxpr  45395  or2expropbilem1  47421  grtriproplem  48328  mo0sn  49204