Theorem bitr4di 197

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr4di.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr4di.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
bitr4di	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4di.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 131	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 195	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr4g  222  bibi2i  226  equsalh  1703  eueq3dc  2882  sbcel12g  3042  sbceqg  3043  sbcnel12g  3044  reldisj  3441  r19.3rm  3478  eldifpr  3583  eldiftp  3601  rabxp  4616  elrng  4770  iss  4905  eliniseg  4949  fcnvres  5346  dffv3g  5457  funimass4  5512  fndmdif  5565  fneqeql  5568  funimass3  5576  elrnrexdmb  5600  dff4im  5606  fconst4m  5680  elunirn  5707  riota1  5788  riota2df  5790  f1ocnvfv3  5803  eqfnov  5917  caoftrn  6047  mpoxopovel  6178  rntpos  6194  ordgt0ge1  6372  iinerm  6541  erinxp  6543  qliftfun  6551  mapdm0  6597  elfi2  6905  fifo  6913  inl11  6995  ctssdccl  7041  isomnimap  7059  ismkvmap  7076  iswomnimap  7088  omniwomnimkv  7089  pr2nelem  7105  indpi  7241  genpdflem  7406  genpdisj  7422  genpassl  7423  genpassu  7424  ltnqpri  7493  ltpopr  7494  ltexprlemm  7499  ltexprlemdisj  7505  ltexprlemloc  7506  ltrennb  7753  letri3  7937  letr  7939  ltneg  8316  leneg  8319  reapltxor  8443  apsym  8460  suprnubex  8803  suprleubex  8804  elnnnn0  9112  zrevaddcl  9196  znnsub  9197  znn0sub  9211  prime  9242  eluz2  9424  eluz2b1  9490  nn01to3  9504  qrevaddcl  9531  xrletri3  9687  xrletr  9690  iccid  9807  elicopnf  9851  fzsplit2  9930  fzsn  9946  fzpr  9957  uzsplit  9972  fvinim0ffz  10118  lt2sqi  10484  le2sqi  10485  abs00ap  10939  iooinsup  11151  mertenslem2  11410  fprod2dlemstep  11496  gcddiv  11874  algcvgblem  11897  isprm3  11966  eltg2b  12393  discld  12475  opnssneib  12495  restbasg  12507  ssidcn  12549  cnptoprest2  12579  lmss  12585  txrest  12615  txlm  12618  imasnopn  12638  bldisj  12740  xmeter  12775  bl2ioo  12881  limcdifap  12970  bj-sseq  13304  nnti  13505  pw1nct  13514