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  8580  dfinfre  9288  sup3exmid  9289  elznn  9664  zq  10035  rpnegap  10097  infssuzex  10676  modqmuladdnn0  10818  shftdm  11601  rexfiuz  11769  rexanuz2  11771  sumsplitdc  12215  fsum2dlemstep  12217  odd2np1  12656  divalgb  12708  nninfctlemfo  12833  isprm4  12913  ctiunctlemudc  13377  grp1  13960  nmznsg  14065  qusecsub  14184  iscrng2  14368  opprsubgg  14439  opprsubrngg  14568  domnmuln0  14631  ringunitsap0  14643  drnguiap  14658  tx1cn  15419  tx2cn  15420  cnbl0  15684  cnblcld  15685  reopnap  15696  pilem1  15930  sinq34lt0t  15982  birthdaylem3  16146  gausslemma2dlem1a  16296  vtxd0nedgbfi  16659