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  2097  reu8  2957  sbc6g  3011  dfss4st  3393  r19.28m  3537  r19.45mv  3541  r19.44mv  3542  r19.27m  3543  ralsnsg  3656  ralsns  3657  iunconstm  3921  iinconstm  3922  exmidsssnc  4233  unisucg  4446  relsng  4763  funssres  5297  fncnv  5321  dff1o5  5510  funimass4  5608  fneqeql2  5668  fnniniseg2  5682  rexsupp  5683  unpreima  5684  dffo3  5706  funfvima  5791  dff13  5812  f1eqcocnv  5835  fliftf  5843  isocnv2  5856  eloprabga  6006  mpo2eqb  6029  opabex3d  6175  opabex3  6176  elxp6  6224  elxp7  6225  sbthlemi5  7022  sbthlemi6  7023  nninfwlporlemd  7233  genpdflem  7569  ltnqpr  7655  ltexprlemloc  7669  xrlenlt  8086  negcon2  8274  dfinfre  8977  sup3exmid  8978  elznn  9336  zq  9694  rpnegap  9755  modqmuladdnn0  10442  shftdm  10969  rexfiuz  11136  rexanuz2  11138  sumsplitdc  11578  fsum2dlemstep  11580  odd2np1  12017  divalgb  12069  infssuzex  12089  nninfctlemfo  12180  isprm4  12260  ctiunctlemudc  12597  grp1  13181  nmznsg  13286  qusecsub  13404  iscrng2  13514  opprsubgg  13583  opprsubrngg  13710  domnmuln0  13772  tx1cn  14448  tx2cn  14449  cnbl0  14713  cnblcld  14714  reopnap  14725  pilem1  14955  sinq34lt0t  15007  gausslemma2dlem1a  15215