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  2136  reu8  3012  sbc6g  3066  dfss4st  3453  r19.28m  3598  r19.45mv  3602  r19.44mv  3603  r19.27m  3604  ralsnsg  3725  ralsns  3726  eldifvsn  3825  iunconstm  3998  iinconstm  3999  exmidsssnc  4315  unisucg  4534  relsng  4852  funssres  5394  fncnv  5421  dff1o5  5622  funimass4  5726  fneqeql2  5786  fnniniseg2  5800  unpreima  5801  dffo3  5823  funfvima  5917  dff13  5940  f1eqcocnv  5963  fliftf  5971  isocnv2  5984  eloprabga  6139  mpo2eqb  6162  opabex3d  6313  opabex3  6314  elxp6  6362  elxp7  6363  mptsuppd  6455  sbthlemi5  7230  sbthlemi6  7231  nninfwlporlemd  7462  genpdflem  7818  ltnqpr  7904  ltexprlemloc  7918  xrlenlt  8334  negcon2  8522  dfinfre  9226  sup3exmid  9227  elznn  9589  zq  9954  rpnegap  10015  infssuzex  10589  modqmuladdnn0  10726  shftdm  11500  rexfiuz  11667  rexanuz2  11669  sumsplitdc  12111  fsum2dlemstep  12113  odd2np1  12552  divalgb  12604  nninfctlemfo  12729  isprm4  12809  ctiunctlemudc  13177  grp1  13808  nmznsg  13919  qusecsub  14037  iscrng2  14148  opprsubgg  14217  opprsubrngg  14345  domnmuln0  14408  tx1cn  15121  tx2cn  15122  cnbl0  15386  cnblcld  15387  reopnap  15398  pilem1  15631  sinq34lt0t  15683  gausslemma2dlem1a  15918  vtxd0nedgbfi  16281