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  2861  necon4abid  2863  uniiunlem  3724  r19.9rzv  4098  inimasn  5585  fnresdisj  6039  f1oiso  6641  reldm  7263  rdglim2  7573  mptelixpg  7987  1idpr  9889  nndiv  11099  fz1sbc  12454  grpid  17504  znleval  19951  fbunfip  21720  lmflf  21856  metcld2  23151  lgsne0  25105  isuvtx  26343  isuvtxaOLD  26344  loopclwwlkn1b  27005  clwwlknun  27087  clwwlknunOLD  27091  frgrncvvdeqlem2  27280  isph  27805  ofpreima  29593  eulerpartlemd  30556  bnj168  30924  opelco3  31802  wl-2sb6d  33471  poimirlem26  33565  cnambfre  33588  heibor1  33739  opltn0  34795  cvrnbtwn2  34880  cvrnbtwn4  34884  atlltn0  34911  pmapjat1  35457  dih1dimatlem  36935  2rexfrabdioph  37677  dnwech  37935  rfovcnvf1od  38615  uneqsn  38638  csbabgOLD  39367  2reu4a  41510  lighneallem2  41848  isrnghm  42217  rnghmval2  42220