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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imimorbdc  908  baib  931  pm5.6dc  938  ifptru  1002  ifpfal  1003  xornbidc  1440  mo2dc  2142  reu8  3022  sbc6g  3076  dfss4st  3464  r19.28m  3617  r19.45mv  3621  r19.44mv  3622  r19.27m  3623  ralsnsg  3746  ralsns  3747  eldifvsn  3847  iunconstm  4020  iinconstm  4021  exmidsssnc  4340  unisucg  4559  relsng  4878  funssres  5420  fncnv  5447  dff1o5  5648  funimass4  5753  fneqeql2  5818  fnniniseg2  5832  unpreima  5833  dffo3  5855  funfvima  5950  dff13  5974  f1eqcocnv  5997  fliftf  6005  isocnv2  6018  eloprabga  6175  mpo2eqb  6198  opabex3d  6350  opabex3  6351  elxp6  6403  elxp7  6404  mptsuppd  6496  sbthlemi5  7278  sbthlemi6  7279  nninfwlporlemd  7513  genpdflem  7875  ltnqpr  7961  ltexprlemloc  7975  xrlenlt  8391  negcon2  8581  dfinfre  9289  sup3exmid  9290  elznn  9665  zq  10036  rpnegap  10098  infssuzex  10677  modqmuladdnn0  10820  shftdm  11603  rexfiuz  11771  rexanuz2  11773  sumsplitdc  12218  fsum2dlemstep  12220  odd2np1  12659  divalgb  12711  nninfctlemfo  12836  isprm4  12916  ctiunctlemudc  13380  grp1  13964  nmznsg  14069  qusecsub  14219  iscrng2  14403  opprsubgg  14474  opprsubrngg  14603  domnmuln0  14666  ringunitsap0  14678  drnguiap  14693  tx1cn  15461  tx2cn  15462  cnbl0  15726  cnblcld  15727  reopnap  15738  pilem1  15972  sinq34lt0t  16024  birthdaylem3  16193  bpos  16286  gausslemma2dlem1a  16348  vtxd0nedgbfi  16711