Theorem bitr4di 198

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 132	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 196	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:  3bitr4g  223  bibi2i  227  3bior1fd  1388  3biant1d  1391  equsalh  1773  eueq3dc  2979  sbcel12g  3141  sbceqg  3142  sbcnel12g  3143  reldisj  3545  r19.3rm  3582  eldifpr  3697  eldiftp  3716  rabxp  4765  elrng  4923  iss  5061  eliniseg  5108  fcnvres  5522  dffv3g  5638  funimass4  5699  fndmdif  5755  fneqeql  5758  funimass3  5766  elrnrexdmb  5790  dff4im  5796  fconst4m  5877  elunirn  5912  riota1  5996  riota2df  5998  f1ocnvfv3  6012  eqfnov  6133  caoftrn  6273  mpoxopovel  6412  rntpos  6428  ordgt0ge1  6608  iinerm  6781  erinxp  6783  qliftfun  6791  mapdm0  6837  elfi2  7176  fifo  7184  inl11  7269  ctssdccl  7315  isomnimap  7341  ismkvmap  7358  iswomnimap  7370  omniwomnimkv  7371  pr2nelem  7401  indpi  7567  genpdflem  7732  genpdisj  7748  genpassl  7749  genpassu  7750  ltnqpri  7819  ltpopr  7820  ltexprlemm  7825  ltexprlemdisj  7831  ltexprlemloc  7832  ltrennb  8079  letri3  8265  letr  8267  ltneg  8647  leneg  8650  reapltxor  8774  apsym  8791  suprnubex  9138  suprleubex  9139  elnnnn0  9450  zrevaddcl  9535  znnsub  9536  znn0sub  9550  prime  9584  eluz2  9766  eluz2b1  9840  nn01to3  9856  qrevaddcl  9883  xrletri3  10044  xrletr  10048  iccid  10165  elicopnf  10209  fzsplit2  10290  fzsn  10306  fzpr  10317  uzsplit  10332  fvinim0ffz  10493  lt2sqi  10895  le2sqi  10896  ccatlcan  11308  ccatrcan  11309  abs00ap  11645  iooinsup  11860  mertenslem2  12120  fprod2dlemstep  12206  gcddiv  12613  algcvgblem  12644  isprm3  12713  dvdsfi  12834  imasmnd2  13558  imasgrp2  13720  issubg  13783  resgrpisgrp  13805  eqgval  13833  imasrng  13993  ring1  14096  imasring  14101  crngunit  14149  lssle0  14410  lssats2  14452  zndvds  14687  znleval  14691  znleval2  14692  eltg2b  14807  discld  14889  opnssneib  14909  restbasg  14921  ssidcn  14963  cnptoprest2  14993  lmss  14999  txrest  15029  txlm  15032  imasnopn  15052  bldisj  15154  xmeter  15189  bl2ioo  15303  limcdifap  15415  issubgr  16137  bj-sseq  16449  nnti  16651  2omap  16654  pw1nct  16664