Theorem syl5rbb 276

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  syl5rbbr  278  necon1abid  3007  necon4abid  3009  uniiunlem  3913  r19.9rzv  4288  inimasn  5804  fnresdisj  6247  f1oiso  6873  reldm  7498  rdglim2  7811  mptelixpg  8231  1idpr  10186  nndiv  11421  fz1sbc  12734  grpid  17844  znleval  20298  fbunfip  22081  lmflf  22217  metcld2  23513  lgsne0  25512  isuvtx  26743  loopclwwlkn1b  27432  clwwlknun  27514  frgrncvvdeqlem2  27708  isph  28249  ofpreima  30030  eulerpartlemd  31026  bnj168  31398  opelco3  32266  wl-2sb6d  33935  poimirlem26  34061  cnambfre  34083  heibor1  34233  opltn0  35344  cvrnbtwn2  35429  cvrnbtwn4  35433  atlltn0  35460  pmapjat1  36007  dih1dimatlem  37483  2rexfrabdioph  38320  dnwech  38577  rfovcnvf1od  39254  uneqsn  39277  2reu4a  42150  lighneallem2  42544  isrnghm  42907  rnghmval2  42910