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  2933  sbc6g  2987  dfss4st  3368  r19.28m  3512  r19.45mv  3516  r19.44mv  3517  r19.27m  3518  ralsnsg  3629  ralsns  3630  iunconstm  3894  iinconstm  3895  exmidsssnc  4202  unisucg  4413  relsng  4728  funssres  5257  fncnv  5281  dff1o5  5469  funimass4  5565  fneqeql2  5624  fnniniseg2  5638  rexsupp  5639  unpreima  5640  dffo3  5662  funfvima  5746  dff13  5766  f1eqcocnv  5789  fliftf  5797  isocnv2  5810  eloprabga  5959  mpo2eqb  5981  opabex3d  6119  opabex3  6120  elxp6  6167  elxp7  6168  sbthlemi5  6957  sbthlemi6  6958  nninfwlporlemd  7167  genpdflem  7503  ltnqpr  7589  ltexprlemloc  7603  xrlenlt  8018  negcon2  8206  dfinfre  8909  sup3exmid  8910  elznn  9265  zq  9622  rpnegap  9682  modqmuladdnn0  10363  shftdm  10824  rexfiuz  10991  rexanuz2  10993  sumsplitdc  11433  fsum2dlemstep  11435  odd2np1  11870  divalgb  11922  infssuzex  11942  isprm4  12111  ctiunctlemudc  12430  grp1  12908  nmznsg  13004  iscrng2  13129  tx1cn  13640  tx2cn  13641  cnbl0  13905  cnblcld  13906  reopnap  13909  pilem1  14071  sinq34lt0t  14123