Theorem 3bitr4i 305

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 280	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 277	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi2d  345  pm4.71  560  pm5.32ri  578  an31  646  pm4.14  805  or4  923  orimdi  927  orbidi  949  ordi  1002  ordir  1003  andir  1005  dfbi3  1044  dfifp7  1064  ifpn  1067  3orrot  1088  3orcoma  1089  3ioran  1102  3ianor  1103  3anbi123i  1151  3orbi123i  1152  an6  1441  3or6  1443  an33rean  1479  nancom  1485  xorcom  1503  xorass  1504  xorbi12i  1513  anxordi  1515  norcom  1519  nornotOLD  1521  norass  1529  hadbi  1594  hadcoma  1595  hadcomaOLD  1596  hadcomb  1597  hadnot  1599  cador  1605  cadan  1606  cadcoma  1609  cadnot  1612  nic-axALT  1671  nfnbi  1851  19.26-3an  1869  19.43OLD  1880  19.32v  1937  19.31v  1938  19.42v  1950  4exdistr  1959  cbvexvw  2040  sbcom4  2095  sbcom3vv  2102  sbal  2162  excom  2165  19.32  2231  19.31  2232  19.42  2234  equsalv  2264  sbex  2284  sbanOLD  2308  sbor  2312  sbbi  2313  sbnvOLD  2318  sbanvOLD  2322  sbbivOLD  2323  cbvexv1  2358  cbvex2v  2361  eeeanv  2367  sbnf2  2373  cbvex2  2430  equsal  2435  dfsb3  2529  dfsb3ALT  2588  sbanALT  2606  sbbiALT  2607  mo4  2646  eu6  2655  eubii  2666  dfeu  2677  sb8eulem  2680  sb8mo  2683  cbvmow  2684  cbveuALT  2688  eu1  2690  sbmo  2694  cbvabv  2889  cbvabw  2890  cbvab  2891  abeq1  2946  nfceqi  2973  sbabel  3015  ralbii2  3163  r19.21v  3175  r2allem  3200  ralcom4  3235  rexbii2  3245  rexanidOLD  3253  reuanid  3328  rmoanid  3329  r19.30OLD  3339  r19.32v  3340  r19.41v  3347  r19.41  3348  r19.42v  3350  r19.43  3351  ralcom  3354  rexcomOLD  3356  ralcomf  3357  rexcomf  3358  reeanlem  3365  3reeanv  3368  2ralor  3369  rabid2  3381  rabid2f  3382  rabbi  3383  reubiia  3390  rmobiia  3395  reu5  3430  rmo5  3434  cbvralfw  3437  cbvrexfw  3438  cbvralf  3439  cbvrexf  3440  cbvreuw  3443  cbvrmow  3444  cbvreu  3447  cbvrmo  3448  cbvralvw  3449  cbvrexvw  3450  vjust  3495  abv  3504  ceqsex3v  3545  ceqsex4v  3546  ceqsex8v  3548  eueq  3698  reu2  3715  reu6  3716  reu3  3717  rmo4  3720  rmo3f  3724  2reu5  3748  cbvsbcw  3803  cbvsbc  3805  sbccomlem  3852  rmo3  3871  rmo3OLD  3872  rmoanim  3877  rmoanimALT  3878  cbvralcsf  3924  cbvrexcsf  3925  cbvreucsf  3926  eqss  3981  uniiunlem  4060  sspsstri  4078  compleq  4123  ssequn1  4155  unss  4159  rexun  4165  ralunb  4166  elin3  4176  incomOLD  4178  inass  4195  ssin  4206  elsymdif  4223  nssinpss  4232  dfun2  4235  difin  4237  indi  4249  indifdir  4259  ssdif0  4322  inssdif0  4328  rabeq0  4337  disj3  4402  ssundif  4432  dfif2  4468  eldifpr  4590  rexsns  4602  snprc  4646  reusn  4656  difsnpss  4733  tpss  4761  pwpr  4825  eluni2  4835  elunirab  4843  uniun  4850  unissb  4862  elintrab  4880  ssintrab  4891  intun  4900  intpr  4901  iuncom  4918  iuncom4  4919  iunab  4967  ssiinf  4970  iunn0  4981  iinab  4982  iunin2  4985  iinun2  4987  iundif2  4988  iunun  5007  iunxun  5008  iunxiun  5011  sspwuni  5014  iinpw  5020  cbvdisj  5033  disjor  5038  brun  5109  brin  5110  brdif  5111  dftr2  5166  intexrab  5235  inuni  5238  ssext  5339  pweqb  5341  otth2  5367  propeqop  5389  opelopabsbALT  5408  eqopab2bw  5427  eqopab2b  5431  pwin  5446  pwun  5452  elxp2  5573  xpiundi  5616  xpiundir  5617  poinxp  5626  soinxp  5627  frinxp  5628  seinxp  5629  weinxp  5630  inopab  5695  difopab  5696  raliunxp  5704  rexiunxp  5705  rexxpf  5712  iunxpf  5713  cnvco  5750  dmiun  5776  dmuni  5777  dm0rn0  5789  dmres  5869  restidsing  5916  cnvsym  5968  asymref  5970  codir  5974  qfto  5975  cnvopab  5991  cnvdif  5996  rniun  6000  dminss  6004  imainss  6005  difxp  6015  xpdifid  6019  dmsnn0  6058  cnvcnvsn  6070  cnvresima  6081  resco  6097  imaco  6098  rnco  6099  coiun  6103  coass  6112  ressn  6130  cnviin  6131  cnvpo  6132  cnvso  6133  xpco  6134  opreu2reurex  6139  dflim2  6241  unisuc  6261  funcnv  6417  funcnv3  6418  fncnv  6421  fun11  6422  imadif  6432  fnres  6468  dfmpt3  6476  mptfnf  6477  fnopabg  6479  fint  6552  fin  6553  fores  6594  dff1o3  6615  f1ompt  6869  fsn  6891  imaiun  6998  isocnv2  7078  isocnv3  7079  isores2  7080  isomin  7084  eqoprab2bw  7218  eqoprab2b  7219  elpwpwel  7483  sucexb  7518  sucelon  7526  dflim4  7557  fiun  7638  f1iun  7639  f11o  7642  opabex3d  7660  opabex3rd  7661  opabex3  7662  dfopab2  7744  dfoprab3s  7745  fmpox  7759  fparlem1  7801  fparlem2  7802  fsplitOLD  7807  suppvalbr  7828  tpostpos  7906  wfrlem8  7956  wfrfun  7959  dfsmo2  7978  brwitnlem  8126  oarec  8182  qsid  8357  uniinqs  8371  mapval2  8430  mapsncnv  8451  elixp2  8459  ixpin  8481  brsdom  8526  brdom2  8533  xpassen  8605  brsdom2  8635  unfilem1  8776  fiint  8789  dfsup2  8902  supmo  8910  eqinf  8942  infmo  8953  rankc1  9293  cp  9314  isinfcard  9512  aceq1  9537  aceq2  9539  dfac5lem3  9545  dfac10b  9559  dfac12a  9568  dffin7-2  9814  dfacfin7  9815  fin1a2lem6  9821  iunfo  9955  konigthlem  9984  axgroth6  10244  axgroth3  10247  sstskm  10258  ltexprlem1  10452  gt0srpr  10494  ltpsrpr  10525  map2psrpr  10526  ltresr  10556  fimaxre3  11581  sup3  11592  supaddc  11602  supmul1  11604  elnn0z  11988  elznn0nn  11989  zmin  12338  xrnemnf  12506  xrnepnf  12507  elioomnf  12826  elxrge0  12839  elfzuzb  12896  fzass4  12939  elfz2nn0  12992  elfzo2  13035  elfzo3  13048  lbfzo0  13071  fzind2  13149  nn0opthlem1  13622  hashgt23el  13779  cotr2g  14330  rexfiuz  14701  fsumcom2  15123  prodmo  15284  fprodcom2  15332  sinltx  15536  divalglem4  15741  divalglem10  15747  4sqlem12  16286  imasleval  16808  xpsfrnel  16829  xpscf  16832  isssc  17084  isffth2  17180  ispos2  17552  ismhm  17952  issubmndb  17964  nsgacs  18308  isgim  18396  oppgcntz  18486  f1omvdco3  18571  pmtrprfvalrn  18610  efgrelexlemb  18870  pgpfac1  19196  pgpfac  19200  issrg  19251  opprsubg  19380  opprunit  19405  isirred2  19445  opprirred  19446  drngprop  19507  opprdrng  19520  issdrg2  19571  islss  19700  islbs  19842  isdomn2  20066  unocv  20818  iunocv  20819  isbasis2g  21550  tgval2  21558  ntreq0  21679  isclo2  21690  cmpcov2  21992  is1stc2  22044  1stcelcls  22063  llyi  22076  unisngl  22129  txuni2  22167  xkobval  22188  hausdiag  22247  isfbas2  22437  elfg  22473  fbasrn  22486  fmfnfmlem3  22558  isfcls  22611  alexsubALTlem2  22650  istmd  22676  istgp  22679  istrg  22766  istdrg  22768  istdrg2  22780  isms2  23054  metuel2  23169  restmetu  23174  isngp  23199  isngp2  23200  isngp3  23201  elii1  23533  isncvsngp  23747  iscph  23768  isbn  23935  pmltpc  24045  ovolfcl  24061  finiunmbl  24139  iundisj  24143  dyaddisj  24191  vitalilem1  24203  ellimc3  24471  ig1pval3  24762  plyun0  24781  plydivex  24880  aannenlem2  24912  ellogrn  25137  atandm  25448  atandm3  25450  atans2  25503  tgjustf  26253  colinearalg  26690  axeuclid  26743  nbgrsym  27139  upgrtrls  27477  upgristrl  27478  usgr2pth0  27540  iswwlks  27608  isclwwlk  27756  clwwlkneq0  27801  h2hlm  28751  issh  28979  chcon2i  29235  chcon1i  29236  chcon3i  29237  chnlei  29256  cmcm2i  29364  cmcm3i  29365  3oalem3  29435  pjdifnormii  29454  pjneli  29494  dfadj2  29656  cnvadj  29663  hhcno  29675  hhcnf  29676  eleigvec  29728  eleigvec2  29729  pjimai  29947  isst  29984  ishst  29985  cvnbtwn4  30060  chrelat4i  30144  2reucom  30237  moel  30246  reuxfrdf  30249  difrab2  30255  inpr0  30286  iunin1f  30303  disjnf  30314  cbvdisjf  30315  disjorf  30323  iundisjf  30333  disjexc  30337  dfrp2  30485  xrdifh  30497  iundisjfi  30513  hashxpe  30523  pmtrprfv2  30727  xrnarchi  30808  isorng  30867  ccfldextdgrr  31052  cmpcref  31109  ordtconnlem1  31162  isrrext  31236  cntnevol  31482  ddemeas  31490  omssubaddlem  31552  omssubadd  31553  eulerpartleme  31616  eulerpartlemv  31617  eulerpartlemt0  31622  eulerpartlemgvv  31629  eulerpartlemn  31634  ballotlem2  31741  ballotlemodife  31750  oddprm2  31921  bnj257  31972  bnj268  31974  bnj290  31975  bnj312  31977  bnj89  31986  bnj887  32031  bnj976  32044  bnj1019  32046  bnj1146  32058  bnj1385  32099  bnj110  32125  bnj121  32137  bnj130  32141  bnj153  32147  bnj543  32160  bnj580  32180  bnj607  32183  bnj849  32192  bnj882  32193  bnj916  32200  bnj985v  32220  bnj985  32221  bnj1033  32236  bnj1083  32245  bnj1090  32246  bnj1128  32257  bnj1174  32270  bnj1228  32278  erdszelem1  32433  cvmliftlem15  32540  snmlval  32573  satfvsuclem2  32602  satfdm  32611  elmpst  32778  mpstrcl  32783  untuni  32930  dfso3  32945  dftr6  32981  coep  32982  coepr  32983  dffr5  32984  dfso2  32985  dfpo2  32986  cnvco1  32990  cnvco2  32991  eldm3  32992  dfdm5  33011  dfrn5  33012  imaindm  33017  frrlem9  33126  elno3  33157  conway  33259  madeval2  33285  brsset  33345  idsset  33346  dfon3  33348  dfbigcup2  33355  dfom5b  33368  dffun10  33370  dfiota3  33379  fnimage  33385  brdomain  33389  brrange  33390  brimg  33393  brapply  33394  brcup  33395  brcap  33396  brsuccf  33397  funpartlem  33398  brrestrict  33405  dfrecs2  33406  brub  33410  altopelaltxp  33432  trer  33659  filnetlem4  33724  df3nandALT1  33742  imnand2  33745  bj-dfbi5  33902  bj-bixor  33920  bj-nnfnt  34064  bj-sbnf  34159  bj-csbsnlem  34215  bj-rcleqf  34332  bj-sscon  34336  bj-restpw  34377  bj-opelidb1  34439  wl-equsalvw  34772  wl-dfrexv  34843  wl-dfrexex  34844  wl-dfrmosb  34847  wl-dfrmov  34848  wl-dfreusb  34851  wl-dfreuv  34852  wl-dfrabv  34856  iundif1  34860  poimirlem25  34911  poimirlem26  34912  poimirlem30  34916  ismblfin  34927  mbfposadd  34933  itg2addnclem2  34938  ftc1anc  34969  inixp  34997  prdstotbnd  35066  heibor1lem  35081  isrngohom  35237  isidl  35286  isfldidl2  35341  isdmn3  35346  sbccom2lem  35396  triantru3  35494  vvdifopab  35515  brres2  35523  eldmqsres  35537  inxpss  35563  n0el2  35584  trcoss2  35718  dfeqvrel2  35819  dfeqvrel3  35820  redundeq1  35858  redundpbi1  35860  refrelredund4  35864  funALTVfun  35925  dfeldisj3  35946  dfeldisj5  35948  pmapglbx  36899  lhpexle3  37142  cdleme25cv  37488  dicelval3  38310  diclspsn  38324  lcfls1c  38666  sn-axrep5v  39101  psspwb  39107  moxfr  39282  fphpd  39406  ifpim1  39827  ifpnot  39828  ifpid2  39829  ifpim2  39830  ifpxorcor  39835  ifpnot23  39837  ifpananb  39865  ifpnannanb  39866  ifpxorxorb  39870  rp-fakeinunass  39874  snen1g  39883  pren2  39905  alephiso2  39910  undmrnresiss  39957  cnvssco  39959  cotrintab  39967  cnviun  39988  imaiun1  39989  coiun1  39990  elintima  39991  frege133d  40103  frege54cor0a  40202  or3or  40364  andi3or  40365  ntrneik4w  40443  k0004lem1  40490  ismnuprim  40623  undisjrab  40631  nzss  40642  pm10.541  40692  compab  40767  onfrALTlem5  40869  onfrALTlem5VD  41212  inn0f  41328  eluni2f  41362  euabsneu  43257  aiotaexb  43283  aiotavb  43284  r19.32  43290  3an4ancom24  43462  ichcom  43611  ichbi12i  43612  ichn  43620  prproropf1olem0  43658  pairreueq  43666  issubmgm  44050  sgrp2sgrp  44129  islindeps  44502  elbigo  44605  setrec1lem3  44786  elpg  44810