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, bitrid 285, bitrdi 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  4275  dfnfc2  4877  ndmima  6078  unfi  9124  axcclem  10400  cshw1  14821  fsumcom2  15773  fprodcom2  15986  pmtr3ncomlem1  19485  mdetunilem7  22647  cmpcov2  23419  hausflf2  24027  conway  27838  umgredg  29274  vtxdginducedm1  29679  2pthfrgrrn  30419  eqdif  32656  padct  32859  cusgredgex2  35411  f1omptsnlem  37768  igenval2  38503  mpobi123f  38599  dmqsblocks  39404  brtrclfv2  44241  clsk1indlem3  44557  permaxpow  45523  permaxpr  45524  or2expropbilem1  47564  grtriproplem  48499  mo0sn  49375