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  896  baib  919  pm5.6dc  926  xornbidc  1391  mo2dc  2081  reu8  2935  sbc6g  2989  dfss4st  3370  r19.28m  3514  r19.45mv  3518  r19.44mv  3519  r19.27m  3520  ralsnsg  3631  ralsns  3632  iunconstm  3896  iinconstm  3897  exmidsssnc  4205  unisucg  4416  relsng  4731  funssres  5260  fncnv  5284  dff1o5  5472  funimass4  5568  fneqeql2  5627  fnniniseg2  5641  rexsupp  5642  unpreima  5643  dffo3  5665  funfvima  5750  dff13  5771  f1eqcocnv  5794  fliftf  5802  isocnv2  5815  eloprabga  5964  mpo2eqb  5986  opabex3d  6124  opabex3  6125  elxp6  6172  elxp7  6173  sbthlemi5  6962  sbthlemi6  6963  nninfwlporlemd  7172  genpdflem  7508  ltnqpr  7594  ltexprlemloc  7608  xrlenlt  8024  negcon2  8212  dfinfre  8915  sup3exmid  8916  elznn  9271  zq  9628  rpnegap  9688  modqmuladdnn0  10370  shftdm  10833  rexfiuz  11000  rexanuz2  11002  sumsplitdc  11442  fsum2dlemstep  11444  odd2np1  11880  divalgb  11932  infssuzex  11952  isprm4  12121  ctiunctlemudc  12440  grp1  12981  nmznsg  13078  iscrng2  13203  tx1cn  13854  tx2cn  13855  cnbl0  14119  cnblcld  14120  reopnap  14123  pilem1  14285  sinq34lt0t  14337