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  2977  necon4abid  2979  uniiunlem  4097  r19.9rzv  4506  2reu4lem  4528  intprg  4986  inimasn  6178  fnresdisj  6689  fnsnfv  6988  f1oiso  7371  reldm  8068  rdglim2  8471  mptelixpg  8974  1idpr  11067  nndiv  12310  fz1sbc  13637  grpid  19006  isrnghm  20458  rnghmval2  20461  znleval  21591  fbunfip  23893  lmflf  24029  metcld2  25355  lgsne0  27394  isuvtx  29427  loopclwwlkn1b  30071  clwwlknun  30141  frgrncvvdeqlem2  30329  isph  30851  ofpreima  32682  fdifsupp  32700  ressply1mon1p  33573  eulerpartlemd  34348  bnj168  34723  cardpred  35083  opelco3  35756  wl-2sb6d  37539  poimirlem26  37633  cnambfre  37655  heibor1  37797  opltn0  39172  cvrnbtwn2  39257  cvrnbtwn4  39261  atlltn0  39288  pmapjat1  39836  dih1dimatlem  41312  2rexfrabdioph  42784  dnwech  43037  rfovcnvf1od  43994  uneqsn  44015  lighneallem2  47531  stgredgiun  47861