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  3974  iinconstm  3975  exmidsssnc  4289  unisucg  4507  relsng  4825  funssres  5364  fncnv  5391  dff1o5  5587  funimass4  5690  fneqeql2  5750  fnniniseg2  5764  rexsupp  5765  unpreima  5766  dffo3  5788  funfvima  5879  dff13  5902  f1eqcocnv  5925  fliftf  5933  isocnv2  5946  eloprabga  6101  mpo2eqb  6124  opabex3d  6276  opabex3  6277  elxp6  6325  elxp7  6326  sbthlemi5  7149  sbthlemi6  7150  nninfwlporlemd  7360  genpdflem  7715  ltnqpr  7801  ltexprlemloc  7815  xrlenlt  8232  negcon2  8420  dfinfre  9124  sup3exmid  9125  elznn  9483  zq  9848  rpnegap  9909  infssuzex  10481  modqmuladdnn0  10618  shftdm  11370  rexfiuz  11537  rexanuz2  11539  sumsplitdc  11980  fsum2dlemstep  11982  odd2np1  12421  divalgb  12473  nninfctlemfo  12598  isprm4  12678  ctiunctlemudc  13045  grp1  13676  nmznsg  13787  qusecsub  13905  iscrng2  14015  opprsubgg  14084  opprsubrngg  14212  domnmuln0  14274  tx1cn  14980  tx2cn  14981  cnbl0  15245  cnblcld  15246  reopnap  15257  pilem1  15490  sinq34lt0t  15542  gausslemma2dlem1a  15774  vtxd0nedgbfi  16101