Theorem syl5rbb 273

Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.)

Hypotheses

Ref	Expression
syl5rbb.1	⊢ (𝜑 ↔ 𝜓)
syl5rbb.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5rbb	⊢ (𝜒 → (𝜃 ↔ 𝜑))

Proof of Theorem syl5rbb

Step	Hyp	Ref	Expression
1		syl5rbb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		syl5rbb.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5bb 272	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 213	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  syl5rbbr  275  necon1abid  2832  necon4abid  2834  uniiunlem  3691  r19.9rzv  4065  inimasn  5550  fnresdisj  6001  f1oiso  6601  reldm  7219  rdglim2  7528  mptelixpg  7945  1idpr  9851  nndiv  11061  fz1sbc  12416  grpid  17457  znleval  19903  fbunfip  21673  lmflf  21809  metcld2  23105  lgsne0  25060  isuvtxa  26295  clwwlksnun  26974  frgrncvvdeqlem2  27164  isph  27677  ofpreima  29465  eulerpartlemd  30428  bnj168  30798  opelco3  31678  wl-2sb6d  33341  poimirlem26  33435  cnambfre  33458  heibor1  33609  opltn0  34477  cvrnbtwn2  34562  cvrnbtwn4  34566  atlltn0  34593  pmapjat1  35139  dih1dimatlem  36618  2rexfrabdioph  37360  dnwech  37618  rfovcnvf1od  38298  uneqsn  38321  csbabgOLD  39050  2reu4a  41189  lighneallem2  41523  isrnghm  41892  rnghmval2  41895