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  904  baib  927  pm5.6dc  934  ifptru  998  ifpfal  999  xornbidc  1436  mo2dc  2138  reu8  3015  sbc6g  3069  dfss4st  3456  r19.28m  3601  r19.45mv  3605  r19.44mv  3606  r19.27m  3607  ralsnsg  3728  ralsns  3729  eldifvsn  3828  iunconstm  4001  iinconstm  4002  exmidsssnc  4318  unisucg  4537  relsng  4855  funssres  5397  fncnv  5424  dff1o5  5625  funimass4  5729  fneqeql2  5789  fnniniseg2  5803  unpreima  5804  dffo3  5826  funfvima  5920  dff13  5943  f1eqcocnv  5966  fliftf  5974  isocnv2  5987  eloprabga  6142  mpo2eqb  6165  opabex3d  6316  opabex3  6317  elxp6  6365  elxp7  6366  mptsuppd  6458  sbthlemi5  7233  sbthlemi6  7234  nninfwlporlemd  7465  genpdflem  7827  ltnqpr  7913  ltexprlemloc  7927  xrlenlt  8343  negcon2  8531  dfinfre  9235  sup3exmid  9236  elznn  9598  zq  9964  rpnegap  10025  infssuzex  10600  modqmuladdnn0  10737  shftdm  11515  rexfiuz  11682  rexanuz2  11684  sumsplitdc  12126  fsum2dlemstep  12128  odd2np1  12567  divalgb  12619  nninfctlemfo  12744  isprm4  12824  ctiunctlemudc  13209  grp1  13840  nmznsg  13951  qusecsub  14069  iscrng2  14180  opprsubgg  14250  opprsubrngg  14379  domnmuln0  14442  ringunitsap0  14454  drnguiap  14469  tx1cn  15183  tx2cn  15184  cnbl0  15448  cnblcld  15449  reopnap  15460  pilem1  15693  sinq34lt0t  15745  gausslemma2dlem1a  15980  vtxd0nedgbfi  16343