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  901  baib  924  pm5.6dc  931  ifptru  995  ifpfal  996  xornbidc  1433  mo2dc  2133  reu8  2999  sbc6g  3053  dfss4st  3437  r19.28m  3581  r19.45mv  3585  r19.44mv  3586  r19.27m  3587  ralsnsg  3703  ralsns  3704  iunconstm  3973  iinconstm  3974  exmidsssnc  4288  unisucg  4506  relsng  4824  funssres  5363  fncnv  5390  dff1o5  5586  funimass4  5689  fneqeql2  5749  fnniniseg2  5763  rexsupp  5764  unpreima  5765  dffo3  5787  funfvima  5878  dff13  5901  f1eqcocnv  5924  fliftf  5932  isocnv2  5945  eloprabga  6100  mpo2eqb  6123  opabex3d  6275  opabex3  6276  elxp6  6324  elxp7  6325  sbthlemi5  7144  sbthlemi6  7145  nninfwlporlemd  7355  genpdflem  7710  ltnqpr  7796  ltexprlemloc  7810  xrlenlt  8227  negcon2  8415  dfinfre  9119  sup3exmid  9120  elznn  9478  zq  9838  rpnegap  9899  infssuzex  10470  modqmuladdnn0  10607  shftdm  11354  rexfiuz  11521  rexanuz2  11523  sumsplitdc  11964  fsum2dlemstep  11966  odd2np1  12405  divalgb  12457  nninfctlemfo  12582  isprm4  12662  ctiunctlemudc  13029  grp1  13660  nmznsg  13771  qusecsub  13889  iscrng2  13999  opprsubgg  14068  opprsubrngg  14196  domnmuln0  14258  tx1cn  14964  tx2cn  14965  cnbl0  15229  cnblcld  15230  reopnap  15241  pilem1  15474  sinq34lt0t  15526  gausslemma2dlem1a  15758  vtxd0nedgbfi  16085