Theorem syl5rbb 272

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 271	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 212	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  syl5rbbr  274  necon1abid  2820  necon4abid  2822  uniiunlem  3653  r19.9rzv  4017  inimasn  5469  fnresdisj  5915  f1oiso  6501  reldm  7110  rdglim2  7415  mptelixpg  7831  1idpr  9730  nndiv  10938  fz1sbc  12285  grpid  17280  znleval  19722  fbunfip  21483  lmflf  21619  metcld2  22913  lgsne0  24860  isph  27061  ofpreima  28848  eulerpartlemd  29755  bnj168  30052  opelco3  30923  wl-2sb6d  32520  poimirlem26  32605  cnambfre  32628  heibor1  32779  opltn0  33495  cvrnbtwn2  33580  cvrnbtwn4  33584  atlltn0  33611  pmapjat1  34157  dih1dimatlem  35636  2rexfrabdioph  36378  dnwech  36636  rfovcnvf1od  37318  uneqsn  37341  csbabgOLD  38072  2reu4a  39838  lighneallem2  40061  isuvtxa  40621  clwwlksnun  41281  isrnghm  41682  rnghmval2  41685