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  898  baib  921  pm5.6dc  928  xornbidc  1411  mo2dc  2110  reu8  2970  sbc6g  3024  dfss4st  3407  r19.28m  3551  r19.45mv  3555  r19.44mv  3556  r19.27m  3557  ralsnsg  3671  ralsns  3672  iunconstm  3937  iinconstm  3938  exmidsssnc  4251  unisucg  4465  relsng  4782  funssres  5318  fncnv  5345  dff1o5  5538  funimass4  5636  fneqeql2  5696  fnniniseg2  5710  rexsupp  5711  unpreima  5712  dffo3  5734  funfvima  5823  dff13  5844  f1eqcocnv  5867  fliftf  5875  isocnv2  5888  eloprabga  6039  mpo2eqb  6062  opabex3d  6213  opabex3  6214  elxp6  6262  elxp7  6263  sbthlemi5  7070  sbthlemi6  7071  nninfwlporlemd  7281  genpdflem  7627  ltnqpr  7713  ltexprlemloc  7727  xrlenlt  8144  negcon2  8332  dfinfre  9036  sup3exmid  9037  elznn  9395  zq  9754  rpnegap  9815  infssuzex  10383  modqmuladdnn0  10520  shftdm  11177  rexfiuz  11344  rexanuz2  11346  sumsplitdc  11787  fsum2dlemstep  11789  odd2np1  12228  divalgb  12280  nninfctlemfo  12405  isprm4  12485  ctiunctlemudc  12852  grp1  13482  nmznsg  13593  qusecsub  13711  iscrng2  13821  opprsubgg  13890  opprsubrngg  14017  domnmuln0  14079  tx1cn  14785  tx2cn  14786  cnbl0  15050  cnblcld  15051  reopnap  15062  pilem1  15295  sinq34lt0t  15347  gausslemma2dlem1a  15579