Theorem bitr2id 283

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

Hypotheses

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

Assertion

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

Proof of Theorem bitr2id

Step	Hyp	Ref	Expression
1		bitr2id.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		bitr2id.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5bb 282	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 222	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitr3di  285  necon1abid  2981  necon4abid  2983  uniiunlem  4015  r19.9rzv  4427  2reu4lem  4453  intprg  4909  inimasn  6048  fnresdisj  6536  fnsnfv  6829  f1oiso  7202  reldm  7858  rdglim2  8234  mptelixpg  8681  1idpr  10716  nndiv  11949  fz1sbc  13261  grpid  18530  znleval  20674  fbunfip  22928  lmflf  23064  metcld2  24376  lgsne0  26388  isuvtx  27665  loopclwwlkn1b  28307  clwwlknun  28377  frgrncvvdeqlem2  28565  isph  29085  ofpreima  30904  eulerpartlemd  32233  bnj168  32609  cardpred  32962  opelco3  33655  wl-2sb6d  35640  poimirlem26  35730  cnambfre  35752  heibor1  35895  opltn0  37131  cvrnbtwn2  37216  cvrnbtwn4  37220  atlltn0  37247  pmapjat1  37794  dih1dimatlem  39270  2rexfrabdioph  40534  dnwech  40789  rfovcnvf1od  41501  uneqsn  41522  lighneallem2  44946  isrnghm  45338  rnghmval2  45341