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  897  baib  920  pm5.6dc  927  xornbidc  1402  mo2dc  2100  reu8  2960  sbc6g  3014  dfss4st  3397  r19.28m  3541  r19.45mv  3545  r19.44mv  3546  r19.27m  3547  ralsnsg  3660  ralsns  3661  iunconstm  3925  iinconstm  3926  exmidsssnc  4237  unisucg  4450  relsng  4767  funssres  5301  fncnv  5325  dff1o5  5516  funimass4  5614  fneqeql2  5674  fnniniseg2  5688  rexsupp  5689  unpreima  5690  dffo3  5712  funfvima  5797  dff13  5818  f1eqcocnv  5841  fliftf  5849  isocnv2  5862  eloprabga  6013  mpo2eqb  6036  opabex3d  6187  opabex3  6188  elxp6  6236  elxp7  6237  sbthlemi5  7036  sbthlemi6  7037  nninfwlporlemd  7247  genpdflem  7591  ltnqpr  7677  ltexprlemloc  7691  xrlenlt  8108  negcon2  8296  dfinfre  9000  sup3exmid  9001  elznn  9359  zq  9717  rpnegap  9778  infssuzex  10340  modqmuladdnn0  10477  shftdm  11004  rexfiuz  11171  rexanuz2  11173  sumsplitdc  11614  fsum2dlemstep  11616  odd2np1  12055  divalgb  12107  nninfctlemfo  12232  isprm4  12312  ctiunctlemudc  12679  grp1  13308  nmznsg  13419  qusecsub  13537  iscrng2  13647  opprsubgg  13716  opprsubrngg  13843  domnmuln0  13905  tx1cn  14589  tx2cn  14590  cnbl0  14854  cnblcld  14855  reopnap  14866  pilem1  15099  sinq34lt0t  15151  gausslemma2dlem1a  15383