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	bitrid 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  2977  necon4abid  2979  uniiunlem  4083  r19.9rzv  4498  2reu4lem  4524  intprg  4984  inimasn  6154  fnresdisj  6669  fnsnfv  6969  f1oiso  7350  reldm  8032  rdglim2  8434  mptelixpg  8931  1idpr  11026  nndiv  12262  fz1sbc  13581  grpid  18896  isrnghm  20332  rnghmval2  20335  znleval  21329  fbunfip  23593  lmflf  23729  metcld2  25055  lgsne0  27074  isuvtx  28919  loopclwwlkn1b  29562  clwwlknun  29632  frgrncvvdeqlem2  29820  isph  30342  ofpreima  32157  ressply1mon1p  32931  eulerpartlemd  33663  bnj168  34039  cardpred  34391  opelco3  35050  wl-2sb6d  36726  poimirlem26  36817  cnambfre  36839  heibor1  36981  opltn0  38363  cvrnbtwn2  38448  cvrnbtwn4  38452  atlltn0  38479  pmapjat1  39027  dih1dimatlem  40503  2rexfrabdioph  41836  dnwech  42092  rfovcnvf1od  43057  uneqsn  43078  lighneallem2  46572