Theorem bitr2id 284

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bitr3di  286  necon1abid  2970  necon4abid  2972  uniiunlem  4062  r19.9rzv  4475  2reu4lem  4497  intprg  4957  inimasn  6145  fnresdisj  6658  fnsnfv  6958  f1oiso  7344  reldm  8043  rdglim2  8446  mptelixpg  8949  1idpr  11043  nndiv  12286  fz1sbc  13617  grpid  18958  isrnghm  20401  rnghmval2  20404  znleval  21515  fbunfip  23807  lmflf  23943  metcld2  25259  lgsne0  27298  isuvtx  29374  loopclwwlkn1b  30023  clwwlknun  30093  frgrncvvdeqlem2  30281  isph  30803  ofpreima  32643  fdifsupp  32662  ressply1mon1p  33581  eulerpartlemd  34398  bnj168  34761  cardpred  35121  opelco3  35792  wl-2sb6d  37576  poimirlem26  37670  cnambfre  37692  heibor1  37834  opltn0  39208  cvrnbtwn2  39293  cvrnbtwn4  39297  atlltn0  39324  pmapjat1  39872  dih1dimatlem  41348  2rexfrabdioph  42819  dnwech  43072  rfovcnvf1od  44028  uneqsn  44049  lighneallem2  47620  stgredgiun  47970  isinito2lem  49383