Theorem bitr4id 199

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 132	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 197	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imimorbdc  901  baib  924  pm5.6dc  931  ifptru  995  ifpfal  996  xornbidc  1433  mo2dc  2133  reu8  3000  sbc6g  3054  dfss4st  3438  r19.28m  3582  r19.45mv  3586  r19.44mv  3587  r19.27m  3588  ralsnsg  3704  ralsns  3705  iunconstm  3976  iinconstm  3977  exmidsssnc  4291  unisucg  4509  relsng  4827  funssres  5366  fncnv  5393  dff1o5  5589  funimass4  5692  fneqeql2  5752  fnniniseg2  5766  rexsupp  5767  unpreima  5768  dffo3  5790  funfvima  5881  dff13  5904  f1eqcocnv  5927  fliftf  5935  isocnv2  5948  eloprabga  6103  mpo2eqb  6126  opabex3d  6278  opabex3  6279  elxp6  6327  elxp7  6328  sbthlemi5  7154  sbthlemi6  7155  nninfwlporlemd  7365  genpdflem  7720  ltnqpr  7806  ltexprlemloc  7820  xrlenlt  8237  negcon2  8425  dfinfre  9129  sup3exmid  9130  elznn  9488  zq  9853  rpnegap  9914  infssuzex  10486  modqmuladdnn0  10623  shftdm  11376  rexfiuz  11543  rexanuz2  11545  sumsplitdc  11986  fsum2dlemstep  11988  odd2np1  12427  divalgb  12479  nninfctlemfo  12604  isprm4  12684  ctiunctlemudc  13051  grp1  13682  nmznsg  13793  qusecsub  13911  iscrng2  14021  opprsubgg  14090  opprsubrngg  14218  domnmuln0  14280  tx1cn  14986  tx2cn  14987  cnbl0  15251  cnblcld  15252  reopnap  15263  pilem1  15496  sinq34lt0t  15548  gausslemma2dlem1a  15780  vtxd0nedgbfi  16110