Theorem 3bitr4i 292

Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
3bitr4i.1	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4i	⊢ (𝜒 ↔ 𝜃)

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 267	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 264	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  bibi2d  332  or4  550  pm4.14  602  pm4.71  662  pm5.32ri  670  an31  841  an4  865  orimdi  892  ordi  908  ordir  909  andir  912  orbidi  973  dfbi3  994  dfbi3OLD  995  dfifp7  1019  ifpn  1022  3anrot  1043  3orrot  1044  3ancoma  1045  3orcoma  1046  3orcomb  1048  3ioran  1056  3anbi123i  1251  3orbi123i  1252  an6  1408  3or6  1410  an33rean  1446  xorcom  1467  xorass  1468  xorbi12i  1477  anxordi  1479  hadbi  1537  hadcoma  1538  hadcomb  1539  hadnot  1541  cador  1547  cadan  1548  cadcoma  1551  cadnot  1554  nic-axALT  1599  nfnbi  1781  19.26-3an  1800  19.43OLD  1811  nfbiiOLD  1836  19.32v  1869  19.31v  1870  sbequ8  1885  19.42v  1918  4exdistr  1924  equsalvw  1931  cbvexvw  1970  excom  2042  19.32  2101  19.31  2102  19.42  2105  equsalv  2108  equsalhw  2123  cbvexv1  2176  eeeanv  2183  cbvex  2272  cbvexv  2275  cbvex2  2280  equsal  2291  dfsb3  2374  sbor  2398  sban  2399  sbbi  2401  sbnf2  2439  sbcom4  2446  sbex  2463  eu5  2496  sb8eu  2503  sb8mo  2504  cbvmo  2506  eu1  2510  sbmo  2515  abeq1  2733  cbvab  2746  sbabel  2793  r2allem  2937  r19.21v  2960  ralbii2  2978  rexbii2  3039  r19.30  3082  r19.32v  3083  r19.41v  3089  r19.41  3090  r19.42v  3092  r19.43  3093  ralcomf  3096  rexcomf  3097  reean  3106  3reeanv  3108  2ralor  3109  rabid2  3118  rabid2f  3119  rabbi  3120  reubiia  3127  rmobiia  3132  reu5  3159  rmo5  3162  cbvralf  3165  cbvrexf  3166  cbvreu  3169  cbvrmo  3170  vjust  3201  abv  3206  ceqsex3v  3246  ceqsex4v  3247  ceqsex8v  3249  eueq  3378  reu2  3394  reu6  3395  reu3  3396  rmo4  3399  2reu5  3416  cbvsbc  3464  sbccomlem  3508  rmo3  3528  cbvralcsf  3565  cbvrexcsf  3566  cbvreucsf  3567  eqss  3618  uniiunlem  3691  sspsstri  3709  compleq  3752  ssequn1  3783  unss  3787  rexun  3793  ralunb  3794  elin3  3804  incom  3805  inass  3823  ssin  3835  elsymdif  3849  elsymdifxor  3850  symdif2  3852  symdifass  3853  nssinpss  3856  dfun2  3859  difin  3861  indi  3873  indifdir  3883  ssdif0  3942  inssdif0  3947  dfnf5  3952  rabeq0  3957  rabn0OLD  3959  disj3  4021  ssundif  4052  dfif2  4088  eldifpr  4204  rexsns  4217  snprc  4253  reusn  4262  difsnpss  4338  prssOLD  4352  tpss  4368  preqsn  4393  pwpr  4430  eluni2  4440  elunirab  4448  uniun  4456  unissb  4469  elintrab  4488  ssintrab  4500  intun  4509  intpr  4510  iuncom  4527  iuncom4  4528  iunab  4566  ssiinf  4569  iunn0  4580  iinab  4581  iunin2  4584  iinun2  4586  iundif2  4587  iunun  4604  iunxun  4605  iunxiun  4608  sspwuni  4611  iinpw  4617  cbvdisj  4630  disjor  4634  brun  4703  brin  4704  brdif  4705  dftr2  4754  intexrab  4823  inuni  4826  ssext  4923  pweqb  4925  otth2  4952  snopeqop  4969  propeqop  4970  opelopabsbALT  4984  eqopab2b  5005  pwin  5018  pwun  5022  elxp2  5132  xpiundi  5173  xpiundir  5174  poinxp  5182  soinxp  5183  frinxp  5184  seinxp  5185  weinxp  5186  inopab  5252  difopab  5253  raliunxp  5261  rexiunxp  5262  rexxpf  5269  iunxpf  5270  cnvco  5308  dmiun  5333  dmuni  5334  dm0rn0  5342  brres  5402  dmres  5419  restidsing  5458  restidsingOLD  5459  cnvsym  5510  asymref  5512  codir  5516  qfto  5517  cnvopab  5533  cnvdif  5539  rniun  5543  dminss  5547  imainss  5548  difxp  5558  xpdifid  5562  dmsnn0  5600  cnvcnvsn  5612  cnvresima  5623  resco  5639  imaco  5640  rnco  5641  coiun  5645  coass  5654  ressn  5671  cnviin  5672  cnvpo  5673  cnvso  5674  xpco  5675  dflim2  5781  unisuc  5801  funcnv  5958  funcnv3  5959  fncnv  5962  fun11  5963  imadif  5973  fnres  6007  dfmpt3  6014  mptfnf  6015  fnopabg  6017  fint  6084  fin  6085  fores  6124  dff1o3  6143  f1ompt  6382  fsn  6402  imaiun  6503  isocnv2  6581  isocnv3  6582  isores2  6583  isomin  6587  eqoprab2b  6713  sucexb  7009  sucelon  7017  dflim4  7048  fun11iun  7126  f11o  7128  opabex3d  7145  opabex3  7146  dfopab2  7222  dfoprab3s  7223  fmpt2x  7236  fparlem1  7277  fparlem2  7278  fsplit  7282  suppvalbr  7299  tpostpos  7372  wfrlem8  7422  wfrfun  7425  dfsmo2  7444  brwitnlem  7587  oarec  7642  qsid  7813  uniinqs  7827  mapval2  7887  mapsncnv  7904  elixp2  7912  ixpin  7933  brsdom  7978  brdom2  7985  xpassen  8054  brsdom2  8084  unfilem1  8224  fiint  8237  dfsup2  8350  supmo  8358  eqinf  8390  infmo  8401  rankc1  8733  cp  8754  isinfcard  8915  aceq1  8940  aceq2  8942  dfac5lem3  8948  dfac10b  8961  dfac12a  8970  dffin7-2  9220  dfacfin7  9221  fin1a2lem6  9227  iunfo  9361  konigthlem  9390  axgroth6  9650  axgroth3  9653  sstskm  9664  ltexprlem1  9858  gt0srpr  9899  ltpsrpr  9930  map2psrpr  9931  ltresr  9961  fimaxre3  10970  sup3  10980  supaddc  10990  supmul1  10992  elnn0z  11390  elznn0nn  11391  zmin  11784  xrnemnf  11951  xrnepnf  11952  elioomnf  12268  elxrge0  12281  elfzuzb  12336  fzass4  12379  elfz2nn0  12431  elfzo2  12473  elfzo3  12486  lbfzo0  12507  fzind2  12586  nn0opthlem1  13055  cotr2g  13715  rexfiuz  14087  fsumcom2  14505  fsumcom2OLD  14506  prodmo  14666  fprodcom2  14714  fprodcom2OLD  14715  sinltx  14919  divalglem4  15119  divalglem10  15125  4sqlem12  15660  imasleval  16201  xpsfrnel  16223  xpscf  16226  isssc  16480  isffth2  16576  ispos2  16948  ismhm  17337  nsgacs  17630  isgim  17704  oppgcntz  17794  f1omvdco3  17869  pmtrprfvalrn  17908  efgrelexlemb  18163  pgpfac1  18479  pgpfac  18483  issrg  18507  opprsubg  18636  opprunit  18661  isirred2  18701  opprirred  18702  drngprop  18758  opprdrng  18771  islss  18935  islbs  19076  isdomn2  19299  unocv  20024  iunocv  20025  fvmptnn04if  20654  isbasis2g  20752  tgval2  20760  ntreq0  20881  isclo2  20892  cmpcov2  21193  is1stc2  21245  1stcelcls  21264  llyi  21277  unisngl  21330  txuni2  21368  xkobval  21389  hausdiag  21448  isfbas2  21639  elfg  21675  fbasrn  21688  fmfnfmlem3  21760  isfcls  21813  alexsubALTlem2  21852  istmd  21878  istgp  21881  istrg  21967  istdrg  21969  istdrg2  21981  isms2  22255  metuel2  22370  restmetu  22375  isngp  22400  isngp2  22401  isngp3  22402  elii1  22734  isncvsngp  22949  iscph  22970  isbn  23135  pmltpc  23219  ovolfcl  23235  finiunmbl  23312  iundisj  23316  dyaddisj  23364  vitalilem1  23376  vitalilem1OLD  23377  ellimc3  23643  ig1pval3  23934  plyun0  23953  plydivex  24052  aannenlem2  24084  ellogrn  24306  atandm  24603  atandm3  24605  atans2  24658  colinearalg  25790  axeuclid  25843  upgrtrls  26598  upgristrl  26599  usgr2pth0  26661  iswwlks  26728  isclwwlks  26880  numclwwlkovf2  27217  h2hlm  27837  issh  28065  chcon2i  28323  chcon1i  28324  chcon3i  28325  chnlei  28344  cmcm2i  28452  cmcm3i  28453  3oalem3  28523  pjdifnormii  28542  pjneli  28582  dfadj2  28744  cnvadj  28751  hhcno  28763  hhcnf  28764  eleigvec  28816  eleigvec2  28817  pjimai  29035  isst  29072  ishst  29073  cvnbtwn4  29148  chrelat4i  29232  moel  29323  rmo3f  29335  rmo4fOLD  29336  difrab2  29339  iunin1f  29374  disjnf  29384  cbvdisjf  29385  disjorf  29392  iundisjf  29402  disjexc  29406  dfrp2  29532  xrdifh  29542  iundisjfi  29555  xrnarchi  29738  isorng  29799  pmtrprfv2  29848  cmpcref  29917  ordtconnlem1  29970  isrrext  30044  cntnevol  30291  ddemeas  30299  omssubaddlem  30361  omssubadd  30362  eulerpartleme  30425  eulerpartlemv  30426  eulerpartlemt0  30431  eulerpartlemgvv  30438  eulerpartlemn  30443  ballotlem2  30550  ballotlemodife  30559  oddprm2  30733  bnj257  30773  bnj268  30775  bnj290  30776  bnj312  30778  bnj89  30787  bnj538OLD  30810  bnj887  30835  bnj976  30848  bnj1019  30850  bnj1146  30862  bnj1385  30903  bnj110  30928  bnj121  30940  bnj130  30944  bnj153  30950  bnj543  30963  bnj580  30983  bnj607  30986  bnj849  30995  bnj882  30996  bnj916  31003  bnj985  31023  bnj1033  31037  bnj1083  31046  bnj1090  31047  bnj1128  31058  bnj1174  31071  bnj1228  31079  erdszelem1  31173  cvmliftlem15  31280  snmlval  31313  elmpst  31433  mpstrcl  31438  untuni  31586  dfso3  31601  dftr6  31640  coep  31641  coepr  31642  dffr5  31643  dfso2  31644  dfpo2  31645  cnvco1  31649  cnvco2  31650  eldm3  31651  dfdm5  31676  dfrn5  31677  imaindm  31682  frrlem5c  31786  elno3  31808  conway  31910  madeval2  31936  brsset  31996  idsset  31997  dfon3  31999  dfbigcup2  32006  dfom5b  32019  dffun10  32021  dfiota3  32030  fnimage  32036  brdomain  32040  brrange  32041  brimg  32044  brapply  32045  brcup  32046  brcap  32047  brsuccf  32048  funpartlem  32049  brrestrict  32056  dfrecs2  32057  brub  32061  altopelaltxp  32083  trer  32310  filnetlem4  32376  df3nandALT1  32396  imnand2  32399  bj-dfbi5  32559  bj-ssbssblem  32649  bj-ssbcom3lem  32650  bj-cbvex2v  32738  bj-abeq1  32774  bj-vjust  32786  bj-sbnf  32828  bj-ralcom4  32868  bj-csbsnlem  32898  bj-sscon  33014  bj-restpw  33045  wl-nancom  33297  iundif1  33383  poimirlem25  33434  poimirlem26  33435  poimirlem30  33439  ismblfin  33450  mbfposadd  33457  itg2addnclem2  33462  ftc1anc  33493  inixp  33523  prdstotbnd  33593  heibor1lem  33608  isrngohom  33764  isidl  33813  isfldidl2  33868  isdmn3  33873  sbccom2lem  33929  triantru3  34000  vvdifopab  34024  brres2  34035  eldmqsres  34051  inxpss  34082  n0el2  34103  pmapglbx  35055  lhpexle3  35298  cdleme25cv  35646  dicelval3  36469  diclspsn  36483  lcfls1c  36825  moxfr  37255  fphpd  37380  issdrg2  37768  ifpim1  37813  ifpnot  37814  ifpid2  37815  ifpim2  37816  ifpxorcor  37821  ifpnot23  37823  ifpananb  37851  ifpnannanb  37852  ifpxorxorb  37856  rp-fakeinunass  37861  undmrnresiss  37910  cnvssco  37912  cotrintab  37921  cnviun  37942  imaiun1  37943  coiun1  37944  elintima  37945  frege133d  38057  frege54cor0a  38157  or3or  38319  andi3or  38320  ntrneikb  38392  ntrneixb  38393  ntrneik4w  38398  k0004lem1  38445  undisjrab  38505  nzss  38516  pm10.541  38566  compab  38645  conss34OLD  38646  onfrALTlem5  38757  csbabgOLD  39050  inn0f  39242  eluni2f  39286  r19.32  41167  rmoanim  41179  issubmgm  41789  sgrp2sgrp  41864  islindeps  42242  elbigo  42345  setrec1lem3  42436  elpg  42457