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  7284  sbthlemi6  7285  nninfwlporlemd  7519  genpdflem  7881  ltnqpr  7967  ltexprlemloc  7981  xrlenlt  8397  negcon2  8587  dfinfre  9295  sup3exmid  9296  elznn  9672  zq  10043  rpnegap  10105  infssuzex  10684  modqmuladdnn0  10827  shftdm  11610  rexfiuz  11778  rexanuz2  11780  sumsplitdc  12225  fsum2dlemstep  12227  odd2np1  12666  divalgb  12718  nninfctlemfo  12843  isprm4  12923  ctiunctlemudc  13387  grp1  13971  nmznsg  14076  qusecsub  14226  iscrng2  14427  opprsubgg  14500  opprsubrngg  14629  domnmuln0  14692  ringunitsap0  14704  drnguiap  14719  tx1cn  15507  tx2cn  15508  cnbl0  15772  cnblcld  15773  reopnap  15784  pilem1  16018  sinq34lt0t  16070  birthdaylem3  16239  bpos  16332  gausslemma2dlem1a  16394  vtxd0nedgbfi  16757