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  2134  reu8  3001  sbc6g  3055  dfss4st  3439  r19.28m  3583  r19.45mv  3587  r19.44mv  3588  r19.27m  3589  ralsnsg  3707  ralsns  3708  iunconstm  3979  iinconstm  3980  exmidsssnc  4295  unisucg  4513  relsng  4831  funssres  5371  fncnv  5398  dff1o5  5595  funimass4  5699  fneqeql2  5759  fnniniseg2  5773  rexsupp  5774  unpreima  5775  dffo3  5797  funfvima  5891  dff13  5914  f1eqcocnv  5937  fliftf  5945  isocnv2  5958  eloprabga  6113  mpo2eqb  6136  opabex3d  6288  opabex3  6289  elxp6  6337  elxp7  6338  sbthlemi5  7165  sbthlemi6  7166  nninfwlporlemd  7376  genpdflem  7732  ltnqpr  7818  ltexprlemloc  7832  xrlenlt  8249  negcon2  8437  dfinfre  9141  sup3exmid  9142  elznn  9500  zq  9865  rpnegap  9926  infssuzex  10499  modqmuladdnn0  10636  shftdm  11405  rexfiuz  11572  rexanuz2  11574  sumsplitdc  12016  fsum2dlemstep  12018  odd2np1  12457  divalgb  12509  nninfctlemfo  12634  isprm4  12714  ctiunctlemudc  13081  grp1  13712  nmznsg  13823  qusecsub  13941  iscrng2  14052  opprsubgg  14121  opprsubrngg  14249  domnmuln0  14311  tx1cn  15022  tx2cn  15023  cnbl0  15287  cnblcld  15288  reopnap  15299  pilem1  15532  sinq34lt0t  15584  gausslemma2dlem1a  15816  vtxd0nedgbfi  16179