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  903  baib  926  pm5.6dc  933  ifptru  997  ifpfal  998  xornbidc  1435  mo2dc  2135  reu8  3002  sbc6g  3056  dfss4st  3440  r19.28m  3584  r19.45mv  3588  r19.44mv  3589  r19.27m  3590  ralsnsg  3706  ralsns  3707  iunconstm  3978  iinconstm  3979  exmidsssnc  4293  unisucg  4511  relsng  4829  funssres  5369  fncnv  5396  dff1o5  5592  funimass4  5696  fneqeql2  5756  fnniniseg2  5770  rexsupp  5771  unpreima  5772  dffo3  5794  funfvima  5886  dff13  5909  f1eqcocnv  5932  fliftf  5940  isocnv2  5953  eloprabga  6108  mpo2eqb  6131  opabex3d  6283  opabex3  6284  elxp6  6332  elxp7  6333  sbthlemi5  7160  sbthlemi6  7161  nninfwlporlemd  7371  genpdflem  7727  ltnqpr  7813  ltexprlemloc  7827  xrlenlt  8244  negcon2  8432  dfinfre  9136  sup3exmid  9137  elznn  9495  zq  9860  rpnegap  9921  infssuzex  10494  modqmuladdnn0  10631  shftdm  11384  rexfiuz  11551  rexanuz2  11553  sumsplitdc  11995  fsum2dlemstep  11997  odd2np1  12436  divalgb  12488  nninfctlemfo  12613  isprm4  12693  ctiunctlemudc  13060  grp1  13691  nmznsg  13802  qusecsub  13920  iscrng2  14031  opprsubgg  14100  opprsubrngg  14228  domnmuln0  14290  tx1cn  14996  tx2cn  14997  cnbl0  15261  cnblcld  15262  reopnap  15273  pilem1  15506  sinq34lt0t  15558  gausslemma2dlem1a  15790  vtxd0nedgbfi  16153