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  2999  sbc6g  3053  dfss4st  3437  r19.28m  3581  r19.45mv  3585  r19.44mv  3586  r19.27m  3587  ralsnsg  3703  ralsns  3704  iunconstm  3973  iinconstm  3974  exmidsssnc  4287  unisucg  4505  relsng  4822  funssres  5360  fncnv  5387  dff1o5  5583  funimass4  5686  fneqeql2  5746  fnniniseg2  5760  rexsupp  5761  unpreima  5762  dffo3  5784  funfvima  5875  dff13  5898  f1eqcocnv  5921  fliftf  5929  isocnv2  5942  eloprabga  6097  mpo2eqb  6120  opabex3d  6272  opabex3  6273  elxp6  6321  elxp7  6322  sbthlemi5  7136  sbthlemi6  7137  nninfwlporlemd  7347  genpdflem  7702  ltnqpr  7788  ltexprlemloc  7802  xrlenlt  8219  negcon2  8407  dfinfre  9111  sup3exmid  9112  elznn  9470  zq  9829  rpnegap  9890  infssuzex  10461  modqmuladdnn0  10598  shftdm  11341  rexfiuz  11508  rexanuz2  11510  sumsplitdc  11951  fsum2dlemstep  11953  odd2np1  12392  divalgb  12444  nninfctlemfo  12569  isprm4  12649  ctiunctlemudc  13016  grp1  13647  nmznsg  13758  qusecsub  13876  iscrng2  13986  opprsubgg  14055  opprsubrngg  14183  domnmuln0  14245  tx1cn  14951  tx2cn  14952  cnbl0  15216  cnblcld  15217  reopnap  15228  pilem1  15461  sinq34lt0t  15513  gausslemma2dlem1a  15745