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  1714  eueq3dc  2900  sbcel12g  3060  sbceqg  3061  sbcnel12g  3062  reldisj  3460  r19.3rm  3497  eldifpr  3603  eldiftp  3622  rabxp  4641  elrng  4795  iss  4930  eliniseg  4974  fcnvres  5371  dffv3g  5482  funimass4  5537  fndmdif  5590  fneqeql  5593  funimass3  5601  elrnrexdmb  5625  dff4im  5631  fconst4m  5705  elunirn  5734  riota1  5816  riota2df  5818  f1ocnvfv3  5831  eqfnov  5948  caoftrn  6075  mpoxopovel  6209  rntpos  6225  ordgt0ge1  6403  iinerm  6573  erinxp  6575  qliftfun  6583  mapdm0  6629  elfi2  6937  fifo  6945  inl11  7030  ctssdccl  7076  isomnimap  7101  ismkvmap  7118  iswomnimap  7130  omniwomnimkv  7131  pr2nelem  7147  indpi  7283  genpdflem  7448  genpdisj  7464  genpassl  7465  genpassu  7466  ltnqpri  7535  ltpopr  7536  ltexprlemm  7541  ltexprlemdisj  7547  ltexprlemloc  7548  ltrennb  7795  letri3  7979  letr  7981  ltneg  8360  leneg  8363  reapltxor  8487  apsym  8504  suprnubex  8848  suprleubex  8849  elnnnn0  9157  zrevaddcl  9241  znnsub  9242  znn0sub  9256  prime  9290  eluz2  9472  eluz2b1  9539  nn01to3  9555  qrevaddcl  9582  xrletri3  9740  xrletr  9744  iccid  9861  elicopnf  9905  fzsplit2  9985  fzsn  10001  fzpr  10012  uzsplit  10027  fvinim0ffz  10176  lt2sqi  10542  le2sqi  10543  abs00ap  11004  iooinsup  11218  mertenslem2  11477  fprod2dlemstep  11563  gcddiv  11952  algcvgblem  11981  isprm3  12050  phisum  12172  eltg2b  12704  discld  12786  opnssneib  12806  restbasg  12818  ssidcn  12860  cnptoprest2  12890  lmss  12896  txrest  12926  txlm  12929  imasnopn  12949  bldisj  13051  xmeter  13086  bl2ioo  13192  limcdifap  13281  bj-sseq  13683  nnti  13884  pw1nct  13893