Theorem bitr4id 198

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
bitr4id	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4id

Step	Hyp	Ref	Expression
1		bitr4id.1	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
2		bitr4id.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	bicomi 131	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 196	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imimorbdc  886  baib  909  pm5.6dc  916  xornbidc  1381  mo2dc  2069  reu8  2922  sbc6g  2975  dfss4st  3355  r19.28m  3498  r19.45mv  3502  r19.44mv  3503  r19.27m  3504  ralsnsg  3613  ralsns  3614  iunconstm  3874  iinconstm  3875  exmidsssnc  4182  unisucg  4392  relsng  4707  funssres  5230  fncnv  5254  dff1o5  5441  funimass4  5537  fneqeql2  5594  fnniniseg2  5608  rexsupp  5609  unpreima  5610  dffo3  5632  funfvima  5716  dff13  5736  f1eqcocnv  5759  fliftf  5767  isocnv2  5780  eloprabga  5929  mpo2eqb  5951  opabex3d  6089  opabex3  6090  elxp6  6137  elxp7  6138  sbthlemi5  6926  sbthlemi6  6927  genpdflem  7448  ltnqpr  7534  ltexprlemloc  7548  xrlenlt  7963  negcon2  8151  dfinfre  8851  sup3exmid  8852  elznn  9207  zq  9564  rpnegap  9622  modqmuladdnn0  10303  shftdm  10764  rexfiuz  10931  rexanuz2  10933  sumsplitdc  11373  fsum2dlemstep  11375  odd2np1  11810  divalgb  11862  infssuzex  11882  isprm4  12051  ctiunctlemudc  12370  tx1cn  12909  tx2cn  12910  cnbl0  13174  cnblcld  13175  reopnap  13178  pilem1  13340  sinq34lt0t  13392