Theorem bitr4id 198

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 131	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 196	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imimorbdc  891  baib  914  pm5.6dc  921  xornbidc  1386  mo2dc  2074  reu8  2926  sbc6g  2979  dfss4st  3360  r19.28m  3504  r19.45mv  3508  r19.44mv  3509  r19.27m  3510  ralsnsg  3620  ralsns  3621  iunconstm  3881  iinconstm  3882  exmidsssnc  4189  unisucg  4399  relsng  4714  funssres  5240  fncnv  5264  dff1o5  5451  funimass4  5547  fneqeql2  5605  fnniniseg2  5619  rexsupp  5620  unpreima  5621  dffo3  5643  funfvima  5727  dff13  5747  f1eqcocnv  5770  fliftf  5778  isocnv2  5791  eloprabga  5940  mpo2eqb  5962  opabex3d  6100  opabex3  6101  elxp6  6148  elxp7  6149  sbthlemi5  6938  sbthlemi6  6939  nninfwlporlemd  7148  genpdflem  7469  ltnqpr  7555  ltexprlemloc  7569  xrlenlt  7984  negcon2  8172  dfinfre  8872  sup3exmid  8873  elznn  9228  zq  9585  rpnegap  9643  modqmuladdnn0  10324  shftdm  10786  rexfiuz  10953  rexanuz2  10955  sumsplitdc  11395  fsum2dlemstep  11397  odd2np1  11832  divalgb  11884  infssuzex  11904  isprm4  12073  ctiunctlemudc  12392  tx1cn  13063  tx2cn  13064  cnbl0  13328  cnblcld  13329  reopnap  13332  pilem1  13494  sinq34lt0t  13546