Theorem bitr2id 286

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitr3di  288  necon1abid  2996  necon4abid  2998  uniiunlem  4041  r19.9rzv  4460  2reu4lem  4478  intprg  4940  inimasn  6141  fnresdisj  6641  fnsnfv  6946  f1oiso  7335  reldm  8025  rdglim2  8403  mptelixpg  8917  1idpr  10998  nndiv  12269  fz1sbc  13615  grpid  19027  isrnghm  20500  rnghmval2  20503  znleval  21613  fbunfip  23936  lmflf  24072  metcld2  25376  lgsne0  27406  sltssnb  27869  isuvtx  29603  loopclwwlkn1b  30251  clwwlknun  30321  frgrncvvdeqlem2  30509  isph  31032  ofpreima  32873  fdifsupp  32893  ressply1mon1p  33767  eulerpartlemd  34665  bnj168  35028  cardpred  35390  opelco3  36130  qdiffALT  37825  wl-2sb6d  38066  poimirlem26  38150  cnambfre  38172  heibor1  38314  opltn0  39819  cvrnbtwn2  39904  cvrnbtwn4  39908  atlltn0  39935  pmapjat1  40482  dih1dimatlem  41958  2rexfrabdioph  43378  dnwech  43630  rfovcnvf1od  44585  uneqsn  44606  lighneallem2  48206  stgredgiun  48571  isinito2lem  50110