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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imimorbdc  908  baib  931  pm5.6dc  938  ifptru  1002  ifpfal  1003  xornbidc  1440  mo2dc  2142  reu8  3022  sbc6g  3076  dfss4st  3464  r19.28m  3617  r19.45mv  3621  r19.44mv  3622  r19.27m  3623  ralsnsg  3746  ralsns  3747  eldifvsn  3847  iunconstm  4020  iinconstm  4021  exmidsssnc  4342  unisucg  4561  relsng  4880  funssres  5423  fncnv  5450  dff1o5  5651  funimass4  5756  fneqeql2  5821  fnniniseg2  5835  unpreima  5836  dffo3  5858  funfvima  5953  dff13  5977  f1eqcocnv  6000  fliftf  6008  isocnv2  6021  eloprabga  6178  mpo2eqb  6201  opabex3d  6354  opabex3  6355  elxp6  6407  elxp7  6408  mptsuppd  6500  sbthlemi5  7285  sbthlemi6  7286  nninfwlporlemd  7518  genpdflem  7880  ltnqpr  7966  ltexprlemloc  7980  xrlenlt  8396  negcon2  8586  dfinfre  9294  sup3exmid  9295  elznn  9669  zq  10041  rpnegap  10103  infssuzex  10682  modqmuladdnn0  10825  shftdm  11608  rexfiuz  11776  rexanuz2  11778  sumsplitdc  12223  fsum2dlemstep  12225  odd2np1  12664  divalgb  12716  nninfctlemfo  12841  isprm4  12921  ctiunctlemudc  13385  grp1  13969  nmznsg  14074  qusecsub  14224  iscrng2  14425  opprsubgg  14498  opprsubrngg  14627  domnmuln0  14690  ringunitsap0  14702  drnguiap  14717  tx1cn  15512  tx2cn  15513  cnbl0  15777  cnblcld  15778  reopnap  15789  pilem1  16023  sinq34lt0t  16075  birthdaylem3  16244  bpos  16337  gausslemma2dlem1a  16399  vtxd0nedgbfi  16762