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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imimorbdc  908  baib  931  pm5.6dc  938  ifptru  1002  ifpfal  1003  xornbidc  1440  mo2dc  2142  reu8  3022  sbc6g  3076  dfss4st  3464  r19.28m  3617  r19.45mv  3621  r19.44mv  3622  r19.27m  3623  ralsnsg  3746  ralsns  3747  eldifvsn  3847  iunconstm  4020  iinconstm  4021  exmidsssnc  4340  unisucg  4559  relsng  4878  funssres  5420  fncnv  5447  dff1o5  5648  funimass4  5753  fneqeql2  5818  fnniniseg2  5832  unpreima  5833  dffo3  5855  funfvima  5950  dff13  5974  f1eqcocnv  5997  fliftf  6005  isocnv2  6018  eloprabga  6175  mpo2eqb  6198  opabex3d  6350  opabex3  6351  elxp6  6403  elxp7  6404  mptsuppd  6496  sbthlemi5  7278  sbthlemi6  7279  nninfwlporlemd  7512  genpdflem  7874  ltnqpr  7960  ltexprlemloc  7974  xrlenlt  8390  negcon2  8579  dfinfre  9287  sup3exmid  9288  elznn  9662  zq  10028  rpnegap  10089  infssuzex  10668  modqmuladdnn0  10807  shftdm  11589  rexfiuz  11757  rexanuz2  11759  sumsplitdc  12201  fsum2dlemstep  12203  odd2np1  12642  divalgb  12694  nninfctlemfo  12819  isprm4  12899  ctiunctlemudc  13330  grp1  13913  nmznsg  14018  qusecsub  14137  iscrng2  14321  opprsubgg  14392  opprsubrngg  14521  domnmuln0  14584  ringunitsap0  14596  drnguiap  14611  tx1cn  15372  tx2cn  15373  cnbl0  15637  cnblcld  15638  reopnap  15649  pilem1  15883  sinq34lt0t  15935  birthdaylem3  16095  gausslemma2dlem1a  16189  vtxd0nedgbfi  16552