Theorem 3bitr4i 303

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  bibi2d  343  pm4.71  559  pm5.32ri  577  an31  647  pm4.14  806  or4  926  orimdi  930  orbidi  952  ordi  1005  ordir  1006  andir  1008  dfbi3  1049  dfifp7  1069  ifpdfbi  1070  ifpn  1073  ifpnOLD  1074  3orrot  1093  3orcoma  1094  3ioran  1107  3ianor  1108  3anbi123i  1156  3orbi123i  1157  an6  1446  3or6  1448  an33rean  1484  an33reanOLD  1485  nancom  1495  xorcomOLD  1514  xorass  1515  xorbi12iOLD  1525  anxordi  1527  norcomOLD  1532  norass  1539  hadbi  1600  hadcoma  1601  hadcomb  1602  hadnot  1604  cador  1610  cadan  1611  cadcoma  1614  cadnot  1617  nic-axALT  1677  nfnbiOLD  1859  19.26-3an  1876  19.43OLD  1887  19.32v  1944  19.31v  1945  19.42v  1958  4exdistr  1966  cbvexvw  2041  exexw  2055  sb3an  2085  sbcom4  2093  sbcom3vv  2099  sbal  2160  excom  2163  19.32  2227  19.31  2228  19.42  2230  equsalv  2259  sbex  2278  sbrim  2301  sbor  2304  sbbi  2305  cbvex2v  2341  eeeanv  2347  sbnf2  2355  cbvsbvf  2361  cbvex2  2412  equsal  2417  dfsb3  2494  mo4  2561  eu6  2569  eubii  2580  dfeu  2590  sb8eulem  2593  sb8mo  2596  cbvmovw  2597  cbvmow  2598  cbvmowOLD  2599  cbveuvw  2601  cbveuw  2602  cbveuALT  2605  eu1  2607  sbmo  2611  cbvabv  2806  cbvabw  2807  cbvabwOLD  2808  cbvab  2809  eqabcb  2876  nfceqi  2901  sbabelOLD  2940  ralbii2  3090  rexbii2  3091  r19.43  3123  r2allem  3143  r19.21vOLD  3181  r19.41v  3189  r19.42v  3191  r19.32v  3192  reeanlem  3226  3reeanv  3228  2ralorOLD  3230  cbvralvw  3235  cbvrexvw  3236  r19.41  3261  ralcom4OLD  3285  ralcom  3287  ralcomf  3300  rexcomf  3301  cbvralfw  3302  cbvralfwOLD  3321  cbvralf  3357  cbvrexf  3358  reu5  3379  rmobiia  3383  reubiia  3384  rmoanidOLD  3389  reuanidOLD  3390  rmo5  3397  cbvrmovw  3400  cbvreuvw  3401  moelOLD  3402  cbvrmow  3406  cbvreuw  3407  cbvrmowOLD  3412  cbvreuwOLD  3413  cbvreu  3425  cbvrmo  3426  rabid2f  3464  rabid2OLD  3466  abv  3486  abvALT  3487  ceqsal  3510  ceqsalv  3512  cgsex4gOLD  3522  ceqsex3v  3532  ceqsex4v  3533  ceqsex8v  3535  reurab  3698  eueq  3705  reu2  3722  reu6  3723  reu3  3724  rmo4  3727  rmo3f  3731  2reu5  3755  cbvsbcw  3812  cbvsbcvw  3813  cbvsbc  3814  sbccomlem  3865  rmo3  3884  rmoanim  3889  rmoanimALT  3890  cbvralcsf  3939  cbvrexcsf  3940  cbvreucsf  3941  dfss2  3969  eqss  3998  uniiunlem  4085  sspsstri  4103  compleq  4148  ssequn1  4181  unss  4185  rexun  4191  ralunb  4192  elin3  4201  inass  4220  ssin  4231  elsymdif  4248  nssinpss  4257  dfun2  4260  difin  4262  indi  4274  indifdi  4284  indifdirOLD  4286  ssdif0  4364  inssdif0  4370  ab0  4375  abn0  4381  rabeq0w  4384  rabeq0  4385  disj  4448  disj3  4454  ssundif  4488  ralidmw  4508  dfif2  4531  eldifpr  4661  rexsns  4674  snprc  4722  reusn  4732  difsnpss  4811  tpss  4839  pwpr  4903  eluni2  4913  elunirab  4925  uniun  4935  unissb  4944  unissbOLD  4945  elintrab  4965  ssintrab  4976  intun  4985  intprOLD  4988  iuncom  5005  iuncom4  5006  iunab  5055  ssiinf  5058  iunn0  5071  iinab  5072  iunin2  5075  iinun2  5077  iundif2  5078  iunun  5097  iunxun  5098  iunxiun  5101  sspwuni  5104  iinpw  5110  cbvdisj  5124  disjor  5129  brun  5200  brin  5201  brdif  5202  dftr2  5268  dftr5  5270  intexrab  5341  inuni  5344  ssext  5455  pweqb  5457  otth2  5484  otthne  5487  propeqop  5508  vopelopabsb  5530  eqopab2bw  5549  eqopab2b  5553  pwin  5571  pwun  5573  dffr6  5635  elxp2  5701  otelxp  5721  xpiundi  5747  xpiundir  5748  poinxp  5757  soinxp  5758  frinxp  5759  seinxp  5760  weinxp  5761  inopab  5830  difopab  5831  difopabOLD  5832  raliunxp  5840  rexiunxp  5841  rexxpf  5848  iunxpf  5849  cnvco  5886  dmiun  5914  dmuni  5915  dm0rn0  5925  dmres  6004  restidsing  6053  cnvsymOLDOLD  6116  asymref  6118  codir  6122  qfto  6123  cnvopab  6139  cnvdif  6144  rniun  6148  dminss  6153  imainss  6154  difxp  6164  xpdifid  6168  dmsnn0  6207  cnvcnvsn  6219  cnvresima  6230  resco  6250  imaco  6251  rnco  6252  coiun  6256  coass  6265  ressn  6285  cnviin  6286  cnvpo  6287  cnvso  6288  xpco  6289  opreu2reurex  6294  dfpo2  6296  imaindm  6299  dflim2  6422  funcnv  6618  funcnv3  6619  fncnv  6622  fun11  6623  imadif  6633  fnres  6678  dfmpt3  6685  mptfnf  6686  fnopabg  6688  fint  6771  fin  6772  fores  6816  dff1o3  6840  f1ompt  7111  fsn  7133  imaiun  7244  isocnv2  7328  isocnv3  7329  isores2  7330  isomin  7334  eqoprab2bw  7479  eqoprab2b  7480  elpwpwel  7754  sucexb  7792  onsucb  7805  dflim4  7837  fiun  7929  f1iun  7930  f11o  7933  opabex3d  7952  opabex3rd  7953  opabex3  7954  dfopab2  8038  dfoprab3s  8039  fmpox  8053  fparlem1  8098  fparlem2  8099  tpostpos  8231  frrlem9  8279  wfrlem8OLD  8316  wfrfunOLD  8319  dfsmo2  8347  brwitnlem  8507  oarec  8562  naddasslem1  8693  naddasslem2  8694  qsid  8777  uniinqs  8791  mapval2  8866  mapsncnv  8887  elixp2  8895  ixpin  8917  brsdom  8971  brdom2  8978  xpassen  9066  brsdom2  9097  dif1enOLD  9162  unfilem1  9310  fiint  9324  dfsup2  9439  supmo  9447  eqinf  9479  infmo  9490  brttrcl2  9709  rankc1  9865  cp  9886  isinfcard  10087  aceq1  10112  aceq2  10114  dfac5lem3  10120  dfac10b  10134  dfac12a  10143  dffin7-2  10393  dfacfin7  10394  fin1a2lem6  10400  iunfo  10534  konigthlem  10563  axgroth6  10823  axgroth3  10826  sstskm  10837  ltexprlem1  11031  gt0srpr  11073  ltpsrpr  11104  map2psrpr  11105  ltresr  11135  fimaxre3  12160  sup3  12171  supaddc  12181  supmul1  12183  elnn0z  12571  elznn0nn  12572  zmin  12928  xrnemnf  13097  xrnepnf  13098  dfrp2  13373  elioomnf  13421  elxrge0  13434  elfzuzb  13495  fzass4  13539  elfz2nn0  13592  elfzo2  13635  elfzo3  13649  lbfzo0  13672  fzind2  13750  nn0opthlem1  14228  hashgt23el  14384  cotr2g  14923  rexfiuz  15294  fsumcom2  15720  prodmo  15880  fprodcom2  15928  sinltx  16132  divalglem4  16339  divalglem10  16345  4sqlem12  16889  imasleval  17487  xpsfrnel  17508  xpscf  17511  isssc  17767  isffth2  17867  ispos2  18268  ismhm  18673  issubmndb  18686  nsgacs  19042  isgim  19136  oppgcntz  19231  f1omvdco3  19317  pmtrprfvalrn  19356  efgrelexlemb  19618  pgpfac1  19950  pgpfac  19954  issrg  20011  opprsubg  20166  opprunit  20191  isirred2  20235  opprirred  20236  drngprop  20372  opprdrng  20389  issdrg2  20411  islss  20545  islbs  20687  isdomn2  20915  unocv  21233  iunocv  21234  isbasis2g  22451  tgval2  22459  ntreq0  22581  isclo2  22592  cmpcov2  22894  is1stc2  22946  1stcelcls  22965  llyi  22978  unisngl  23031  txuni2  23069  xkobval  23090  hausdiag  23149  isfbas2  23339  elfg  23375  fbasrn  23388  fmfnfmlem3  23460  isfcls  23513  alexsubALTlem2  23552  istmd  23578  istgp  23581  istrg  23668  istdrg  23670  istdrg2  23682  isms2  23956  metuel2  24074  restmetu  24079  isngp  24105  isngp2  24106  isngp3  24107  elii1  24451  isncvsngp  24666  iscph  24687  isbn  24855  pmltpc  24967  ovolfcl  24983  finiunmbl  25061  iundisj  25065  dyaddisj  25113  vitalilem1  25125  ellimc3  25396  ig1pval3  25692  plyun0  25711  plydivex  25810  aannenlem2  25842  ellogrn  26068  atandm  26381  atandm3  26383  atans2  26436  elno3  27158  conway  27300  eqscut2  27307  madeval2  27348  tgjustf  27724  colinearalg  28168  axeuclid  28221  nbgrsym  28620  upgrtrls  28958  upgristrl  28959  usgr2pth0  29022  iswwlks  29090  isclwwlk  29237  clwwlkneq0  29282  h2hlm  30233  issh  30461  chcon2i  30717  chcon1i  30718  chcon3i  30719  chnlei  30738  cmcm2i  30846  cmcm3i  30847  3oalem3  30917  pjdifnormii  30936  pjneli  30976  dfadj2  31138  cnvadj  31145  hhcno  31157  hhcnf  31158  eleigvec  31210  eleigvec2  31211  pjimai  31429  isst  31466  ishst  31467  cvnbtwn4  31542  chrelat4i  31626  2reucom  31720  reuxfrdf  31731  difrab2  31738  inpr0  31769  iunin1f  31789  disjnf  31801  cbvdisjf  31802  disjorf  31810  iundisjf  31820  disjexc  31824  xrdifh  31991  iundisjfi  32007  hashxpe  32019  pmtrprfv2  32249  xrnarchi  32330  isorng  32417  prmidl0  32569  opprnsg  32598  ccfldextdgrr  32746  cmpcref  32830  ordtconnlem1  32904  isrrext  32980  cntnevol  33226  ddemeas  33234  omssubaddlem  33298  omssubadd  33299  eulerpartleme  33362  eulerpartlemv  33363  eulerpartlemt0  33368  eulerpartlemgvv  33375  eulerpartlemn  33380  ballotlem2  33487  ballotlemodife  33496  oddprm2  33667  bnj257  33718  bnj268  33720  bnj290  33721  bnj312  33723  bnj89  33732  bnj887  33776  bnj976  33788  bnj1019  33790  bnj1146  33802  bnj1385  33843  bnj110  33869  bnj121  33881  bnj130  33885  bnj153  33891  bnj543  33904  bnj580  33924  bnj607  33927  bnj849  33936  bnj882  33937  bnj916  33944  bnj985v  33964  bnj985  33965  bnj1033  33980  bnj1083  33989  bnj1090  33990  bnj1128  34001  bnj1174  34014  bnj1228  34022  erdszelem1  34182  cvmliftlem15  34289  snmlval  34322  satfvsuclem2  34351  satfdm  34360  elmpst  34527  mpstrcl  34532  untuni  34678  dfso3  34689  xpab  34695  dftr6  34721  coep  34722  coepr  34723  dffr5  34724  dfso2  34725  cnvco1  34729  cnvco2  34730  eldm3  34731  dfdm5  34744  dfrn5  34745  brsset  34861  idsset  34862  dfon3  34864  dfbigcup2  34871  dfom5b  34884  dffun10  34886  dfiota3  34895  fnimage  34901  brdomain  34905  brrange  34906  brimg  34909  brapply  34910  brcup  34911  brcap  34912  brsuccf  34913  funpartlem  34914  brrestrict  34921  dfrecs2  34922  brub  34926  altopelaltxp  34948  trer  35201  filnetlem4  35266  df3nandALT1  35284  imnand2  35287  bj-dfbi5  35451  bj-bixor  35469  bj-nnfnt  35618  bj-sbnf  35719  bj-csbsnlem  35783  bj-rcleqf  35906  bj-sscon  35910  bj-pw0ALT  35930  bj-restpw  35973  bj-opelidb1  36034  bj-imdiridlem  36066  bj-imdirco  36071  wl-df3xor2  36350  wl-3xorrot  36358  wl-3xorcoma  36359  wl-3xornot  36362  wl-df2-3mintru2  36366  wl-df3-3mintru2  36367  wl-df4-3mintru2  36368  wl-equsalvw  36407  iundif1  36462  poimirlem25  36513  poimirlem26  36514  poimirlem30  36518  ismblfin  36529  mbfposadd  36535  itg2addnclem2  36540  ftc1anc  36569  inixp  36596  prdstotbnd  36662  heibor1lem  36677  isrngohom  36833  isidl  36882  isfldidl2  36937  isdmn3  36942  sbccom2lem  36992  triantru3  37094  vvdifopab  37128  brres2  37136  eldmqsres  37155  inxpss  37180  ref5  37182  n0el2  37202  trcoss2  37354  dfeqvrel2  37460  dfeqvrel3  37461  redundeq1  37499  redundpbi1  37501  refrelredund4  37505  funALTVfun  37568  dfeldisj3  37589  dfeldisj5  37591  pet0  37685  petid  37687  petidres  37689  petinidres  37691  petxrnidres  37693  mpet  37709  petincnvepres  37719  pet  37721  pmapglbx  38640  lhpexle3  38883  cdleme25cv  39229  dicelval3  40051  diclspsn  40065  lcfls1c  40407  sn-axrep5v  41033  sn-iotalem  41038  psspwb  41046  moxfr  41430  fphpd  41554  uniel  41966  dflim6  42014  onsucf1olem  42020  dflim7  42023  omge2  42048  oenassex  42068  safesnsupfilb  42169  ifpim1  42220  ifpnot  42221  ifpid2  42222  ifpim2  42223  ifpxorcor  42227  ifpnot23  42229  ifpananb  42257  ifpnannanb  42258  ifpxorxorb  42262  rp-fakeinunass  42266  snen1g  42275  pren2  42304  alephiso2  42309  undmrnresiss  42355  cnvssco  42357  cotrintab  42365  cnviun  42401  imaiun1  42402  coiun1  42403  elintima  42404  frege133d  42516  frege54cor0a  42614  or3or  42774  andi3or  42775  ntrneik4w  42851  k0004lem1  42898  ismnuprim  43053  ismnushort  43060  undisjrab  43065  nzss  43076  pm10.541  43126  compab  43201  onfrALTlem5  43303  onfrALTlem5VD  43646  inn0f  43760  eluni2f  43792  euabsneu  45738  aiotaexb  45797  aiotavb  45798  r19.32  45806  3an4ancom24  45977  ichn  46124  ichcom  46127  ichbi12i  46128  prproropf1olem0  46170  pairreueq  46178  issubmgm  46559  sgrp2sgrp  46638  islindeps  47134  elbigo  47237  reutruALT  47491  isthincd2  47658  setrec1lem3  47734  elpg  47759