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  882  baib  905  pm5.6dc  912  xornbidc  1370  mo2dc  2058  reu8  2904  sbc6g  2957  dfss4st  3336  r19.28m  3479  r19.45mv  3483  r19.44mv  3484  r19.27m  3485  ralsnsg  3592  ralsns  3593  iunconstm  3853  iinconstm  3854  exmidsssnc  4159  unisucg  4369  relsng  4682  funssres  5205  fncnv  5229  dff1o5  5416  funimass4  5512  fneqeql2  5569  fnniniseg2  5583  rexsupp  5584  unpreima  5585  dffo3  5607  funfvima  5689  dff13  5709  f1eqcocnv  5732  fliftf  5740  isocnv2  5753  eloprabga  5898  mpo2eqb  5920  opabex3d  6059  opabex3  6060  elxp6  6107  elxp7  6108  sbthlemi5  6894  sbthlemi6  6895  genpdflem  7406  ltnqpr  7492  ltexprlemloc  7506  xrlenlt  7921  negcon2  8107  dfinfre  8806  sup3exmid  8807  elznn  9162  zq  9513  rpnegap  9571  modqmuladdnn0  10245  shftdm  10699  rexfiuz  10866  rexanuz2  10868  sumsplitdc  11306  fsum2dlemstep  11308  odd2np1  11737  divalgb  11789  infssuzex  11809  isprm4  11967  ctiunctlemudc  12117  tx1cn  12608  tx2cn  12609  cnbl0  12873  cnblcld  12874  reopnap  12877  pilem1  13039  sinq34lt0t  13091