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  900  baib  923  pm5.6dc  930  xornbidc  1413  mo2dc  2113  reu8  2979  sbc6g  3033  dfss4st  3417  r19.28m  3561  r19.45mv  3565  r19.44mv  3566  r19.27m  3567  ralsnsg  3683  ralsns  3684  iunconstm  3952  iinconstm  3953  exmidsssnc  4266  unisucg  4482  relsng  4799  funssres  5336  fncnv  5363  dff1o5  5557  funimass4  5657  fneqeql2  5717  fnniniseg2  5731  rexsupp  5732  unpreima  5733  dffo3  5755  funfvima  5844  dff13  5865  f1eqcocnv  5888  fliftf  5896  isocnv2  5909  eloprabga  6062  mpo2eqb  6085  opabex3d  6236  opabex3  6237  elxp6  6285  elxp7  6286  sbthlemi5  7096  sbthlemi6  7097  nninfwlporlemd  7307  genpdflem  7662  ltnqpr  7748  ltexprlemloc  7762  xrlenlt  8179  negcon2  8367  dfinfre  9071  sup3exmid  9072  elznn  9430  zq  9789  rpnegap  9850  infssuzex  10420  modqmuladdnn0  10557  shftdm  11299  rexfiuz  11466  rexanuz2  11468  sumsplitdc  11909  fsum2dlemstep  11911  odd2np1  12350  divalgb  12402  nninfctlemfo  12527  isprm4  12607  ctiunctlemudc  12974  grp1  13605  nmznsg  13716  qusecsub  13834  iscrng2  13944  opprsubgg  14013  opprsubrngg  14140  domnmuln0  14202  tx1cn  14908  tx2cn  14909  cnbl0  15173  cnblcld  15174  reopnap  15185  pilem1  15418  sinq34lt0t  15470  gausslemma2dlem1a  15702