Theorem 3bitr4i 306

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi2d  345  pm4.71  567  pm5.32ri  586  an31  661  pm4.14  819  or4  940  orimdi  944  orbidi  967  ordi  1023  ordir  1024  andir  1026  dfbi3  1065  dfifp7  1085  ifpdfbiOLD  1087  ifpn  1090  3orrot  1108  3orcoma  1109  3ioran  1123  3ianor  1124  3anbi123i  1173  3orbi123i  1174  3jaob  1453  an6  1474  3or6  1476  an3andi  1513  an33rean  1514  nancom  1526  xorass  1545  anxordi  1556  norass  1567  hadbi  1628  hadcoma  1629  hadcomb  1630  hadnot  1632  cador  1641  cadan  1642  cadcoma  1645  cadnot  1648  nic-axALT  1707  19.26-3an  1905  19.43OLD  1916  19.32v  1973  19.31v  1974  19.42v  1986  4exdistr  1994  cbvexvw  2070  exexw  2086  sb3an  2118  sbcom4  2126  sbbiiev  2130  excom  2200  sbal  2207  19.32  2272  19.31  2273  19.42  2275  equsalv  2305  sbex  2318  sbrim  2341  sbor  2343  sbbi  2344  cbvex2v  2378  eeeanv  2384  sbnf2  2392  cbvsbvf  2397  cbvex2  2446  equsal  2451  dfsb3  2528  mo4  2596  eu6  2604  dfeu  2625  sb8eulem  2628  sb8mo  2631  cbvmovw  2632  cbvmow  2633  cbveuvw  2635  cbveuw  2636  cbveuALT  2638  eu1  2640  sbmo  2644  cbvabv  2835  cbvabw  2836  cbvab  2837  eqabcbw  2839  eqabcb  2905  nfceqi  2924  ralbii2  3109  rexbii2  3110  r19.26-3  3128  r19.43  3135  r2allem  3155  r19.42v  3199  r19.32v  3200  reeanlem  3238  3reeanv  3240  cbvralvw  3245  cbvrexvw  3246  ralcom  3295  ralcomf  3305  rexcomf  3306  cbvralfw  3307  cbvralsvw  3318  cbvralf  3351  cbvrexf  3352  reu5  3373  rmobiia  3377  reubiia  3378  rmo5  3389  cbvrmovw  3392  cbvreuvw  3393  cbvrmow  3396  cbvreuw  3397  cbvreu  3410  cbvrmo  3411  rabid2f  3449  abv  3469  abvALT  3470  ceqsal  3494  ceqsalv  3496  ceqsex3v  3509  ceqsex4v  3510  ceqsex8v  3512  reurab  3666  eueq  3673  reu2  3690  reu6  3691  reu3  3692  rmo4  3695  rmo3f  3699  2reu5  3723  cbvsbcw  3779  cbvsbcvw  3780  cbvsbc  3781  sbc3an  3810  rmo3  3843  rmoanim  3849  rmoanimALT  3850  cbvralcsf  3896  cbvrexcsf  3897  cbvreucsf  3898  eqss  3953  uniiunlem  4042  sspsstri  4061  compleq  4106  ssequn1  4139  unss  4143  rexun  4149  ralunb  4150  elin3  4159  inass  4180  ssin  4191  elsymdif  4211  nssinpss  4220  dfun2  4223  difin  4225  indi  4237  indifdi  4247  difin2  4254  eq0  4304  ssdif0  4321  inn0f  4326  inssdif0OLD  4330  ab0w  4335  ab0  4336  ab0orv  4339  abn0  4341  rabeq0w  4344  rabeq0  4345  disj3  4414  ssundif  4450  ralidmw  4479  dfif2  4491  eldifpr  4626  rexdifpr  4627  rexsns  4639  snprc  4685  reusn  4695  difsnpss  4777  tpss  4804  pwpr  4868  eluni2  4878  elunirab  4889  uniun  4897  unissb  4908  elintrab  4927  ssintrab  4938  intun  4947  iuncom  4966  iuncom4  4967  iunab  5018  ssiinf  5021  iunn0  5033  iinab  5034  iunin2  5037  iinun2  5039  iundif2  5040  iunun  5061  iunxun  5062  iunxiun  5065  sspwuni  5068  iinpw  5074  cbvdisj  5088  cbvdisjv  5089  disjor  5093  brun  5164  brin  5165  brdif  5166  dftr2  5222  dftr5  5224  intexrab  5319  inuni  5322  ssext  5437  pweqb  5439  otth2  5467  otthne  5470  propeqop  5492  vopelopabsb  5515  eqopab2bw  5535  eqopab2b  5539  pwin  5554  pwun  5556  dffr6  5619  elxp2  5687  otelxp  5707  xpiundi  5734  xpiundir  5735  poinxp  5744  soinxp  5745  frinxp  5746  seinxp  5747  weinxp  5748  reliun  5805  inopab  5818  difopab  5819  inxp  5820  raliunxp  5827  rexiunxp  5828  rexxpf  5835  iunxpf  5836  cnvco  5877  dmiun  5905  dmuni  5906  dm0rn0  5916  dm0rn0OLD  5917  dmres  6013  restidsing  6057  asymref  6118  codir  6122  qfto  6123  cnvopab  6139  cnvdif  6142  rniun  6147  dminss  6152  imainss  6153  difxp  6163  xpdifid  6167  xpdifcnvepel  6168  dmsnn0  6210  cnvcnvsn  6222  cnvresima  6233  resco  6253  imaco  6254  rnco  6255  rncoOLD  6256  coiun  6260  coass  6269  ressn  6290  cnviin  6291  cnvpo  6292  cnvso  6293  xpco  6294  opreu2reurex  6299  dfpo2  6301  imaindm  6304  dflim2  6423  funcnv  6609  funcnv3  6610  fncnv  6613  fun11  6614  imadif  6624  fnres  6666  dfmpt3  6673  mptfnf  6674  fnopabg  6676  fint  6761  fin  6762  fores  6806  dff1o3  6831  f1ompt  7110  fsn  7135  imaiun  7248  isocnv2  7338  isocnv3  7339  isores2  7340  isomin  7344  eqoprab2bw  7489  eqoprab2b  7490  elpwpwel  7772  sucexb  7809  onsucb  7819  dflim4  7850  fiun  7946  f1iun  7947  f11o  7950  opabex3d  7968  opabex3rd  7969  opabex3  7970  dfopab2  8055  dfoprab3s  8056  fmpox  8070  fparlem1  8113  fparlem2  8114  tpostpos  8248  frrlem9  8297  dfsmo2  8340  brwitnlem  8498  oarec  8553  naddasslem1  8687  naddasslem2  8688  qsid  8785  uniinqs  8801  mapval2  8876  mapsncnv  8897  elixp2  8905  ixpin  8927  brsdom  8977  brdom2  8985  xpassen  9066  brsdom2  9096  unfilem1  9272  fiint  9293  dfsup2  9411  supmo  9419  eqinf  9452  infmo  9464  brttrcl2  9690  rankc1  9849  cp  9890  isinfcard  10092  aceq1  10117  aceq2  10119  dfac5lem3  10125  dfac10b  10139  dfac12a  10148  dffin7-2  10397  dfacfin7  10398  fin1a2lem6  10404  iunfo  10538  konigthlem  10568  axgroth6  10828  axgroth3  10831  sstskm  10842  ltexprlem1  11036  gt0srpr  11078  ltpsrpr  11109  map2psrpr  11110  ltresr  11140  fimaxre3  12176  sup3  12187  supaddc  12197  supmul1  12199  elnn0z  12619  elznn0nn  12620  zmin  12984  xrnemnf  13158  xrnepnf  13159  dfrp2  13437  elioomnf  13487  elxrge0  13500  elfzuzb  13562  fzass4  13607  elfz2nn0  13663  elfzo2  13707  elfzo3  13722  lbfzo0  13745  fzo1lb  13759  fzind2  13834  nn0opthlem1  14322  hashgt23el  14479  cotr2g  15037  rexfiuz  15423  fsumcom2  15848  prodmo  16013  fprodcom2  16061  sinltx  16267  divalglem4  16476  divalglem10  16482  4sqlem12  17038  imasleval  17617  xpsfrnel  17638  xpscf  17641  isssc  17899  isffth2  17997  ispos2  18393  issubmgm  18792  ismhm  18880  issubmndb  18900  nsgacs  19272  isgim  19376  oppgcntz  19478  f1omvdco3  19563  pmtrprfvalrn  19602  efgrelexlemb  19864  pgpfac1  20196  pgpfac  20200  issrg  20314  opprsubg  20480  opprunit  20505  isirred2  20549  opprirred  20550  isrhm0  20604  opprnzrb  20669  opprdomnb  20865  isdomn4r  20867  drngprop  20894  isdrng3  20903  isdrng5  20904  opprdrng  20917  issdrg2  20948  isorng  21014  islss  21105  islbs  21247  isfieldidl  21436  isfieldidl2  21437  prmidl0  21528  unocv  21880  iunocv  21881  isbasis2g  23155  tgval2  23163  ntreq0  23284  isclo2  23295  cmpcov2  23597  is1stc2  23649  1stcelcls  23669  llyi  23682  unisngl  23735  txuni2  23773  xkobval  23794  hausdiag  23853  isfbas2  24043  elfg  24079  fbasrn  24092  fmfnfmlem3  24164  isfcls  24217  alexsubALTlem2  24256  istmd  24282  istgp  24285  istrg  24372  istdrg  24374  istdrg2  24386  isms2  24658  metuel2  24773  restmetu  24778  isngp  24804  isngp2  24805  isngp3  24806  elii1  25145  isncvsngp  25359  iscph  25380  isbn  25548  pmltpc  25660  ovolfcl  25676  finiunmbl  25754  iundisj  25758  dyaddisj  25806  vitalilem1  25818  ellimc3  26089  ig1pval3  26386  plyun0  26405  plydivex  26509  aannenlem2  26543  ellogrn  26775  atandm  27092  atandm3  27094  atans2  27147  elno3  27870  conway  28023  eqcuts2  28030  madeval2  28077  ons2ind  28519  tgjustf  28793  colinearalg  29315  axeuclid  29368  nbgrsym  29771  upgrtrls  30111  upgristrl  30112  dfpth2  30141  usgr2pth0  30178  iswwlks  30252  isclwwlk  30402  clwwlkneq0  30447  h2hlm  31403  issh  31631  chcon2i  31887  chcon1i  31888  chcon3i  31889  chnlei  31908  cmcm2i  32016  cmcm3i  32017  3oalem3  32087  pjdifnormii  32106  pjneli  32146  dfadj2  32308  cnvadj  32315  hhcno  32327  hhcnf  32328  eleigvec  32380  eleigvec2  32381  pjimai  32599  isst  32636  ishst  32637  cvnbtwn4  32712  chrelat4i  32796  2reucom  32897  reuxfrdf  32908  difrab2  32915  inpr0  32949  iunin1f  32973  disjnf  32986  cbvdisjf  32987  disjorf  32995  iundisjf  33005  disjexc  33009  xrdifh  33195  iundisjfi  33211  hashxpe  33222  pmtrprfv2  33472  xrnarchi  33568  isunit2  33623  opprnsg  33830  ccfldextdgrr  34126  cmpcref  34304  ordtconnlem1  34378  isrrext  34454  cntnevol  34683  ddemeas  34691  omssubaddlem  34754  omssubadd  34755  eulerpartleme  34818  eulerpartlemv  34819  eulerpartlemt0  34824  eulerpartlemgvv  34831  eulerpartlemn  34836  ballotlem2  34944  ballotlemodife  34953  oddprm2  35107  bnj257  35161  bnj268  35163  bnj290  35164  bnj312  35166  bnj89  35175  bnj887  35219  bnj976  35231  bnj1019  35233  bnj1146  35244  bnj1385  35285  bnj110  35311  bnj121  35323  bnj130  35327  bnj153  35333  bnj543  35346  bnj580  35366  bnj607  35369  bnj849  35378  bnj882  35379  bnj916  35386  bnj985v  35406  bnj985  35407  bnj1033  35422  bnj1083  35431  bnj1090  35432  bnj1128  35443  bnj1174  35456  bnj1228  35464  onvf1odlem1  35644  erdszelem1  35720  cvmliftlem15  35827  snmlval  35860  satfvsuclem2  35889  satfdm  35898  elmpst  36065  mpstrcl  36070  orbi2iALT  36214  untuni  36238  dfso3  36249  xpab  36255  dftr6  36280  coep  36281  coepr  36282  dffr5  36283  dfso2  36284  cnvco1  36288  cnvco2  36289  eldm3  36290  dfdm5  36302  dfrn5  36303  brsset  36416  idsset  36417  dfon3  36419  dfbigcup2  36426  dfom5b  36439  dffun10  36441  dfiota3  36450  fnimage  36456  brdomain  36460  brrange  36461  brimg  36464  brapply  36465  brcup  36466  brcap  36467  lemsuccf  36468  funpartlem  36471  brrestrict  36478  dfrecs2  36479  brub  36483  altopelaltxp  36505  ltnadd  36747  rmoeqi  36756  rmoeqbii  36757  reueqi  36758  reueqbii  36759  sbceqbii  36760  disjeq1i  36761  cbvralvw2  36795  cbvrexvw2  36796  cbvrmovw2  36797  cbvreuvw2  36798  cbvsbcvw2  36799  cbvdisjvw2  36804  trer  36884  filnetlem4  36949  df3nandALT1  36967  imnand2  36970  mh-unprimbi  37112  bj-dfbi5  37224  bj-bixor  37241  bj-dfsbc  37331  bj-nnfnt  37432  bj-csbsnlem  37595  bj-rcleqf  37718  bj-sscon  37722  bj-pw0ALT  37742  bj-restpw  37791  bj-opelidb1  37854  bj-imdiridlem  37886  bj-imdirco  37891  wl-df3xor2  38172  wl-3xorrot  38180  wl-3xorcoma  38181  wl-3xornot  38184  wl-df2-3mintru2  38188  wl-df3-3mintru2  38189  wl-df4-3mintru2  38190  wl-equsalvw  38250  wl-sb9v  38261  iundif1  38302  poimirlem25  38353  poimirlem26  38354  poimirlem30  38358  ismblfin  38369  mbfposadd  38375  itg2addnclem2  38380  ftc1anc  38409  inixp  38437  prdstotbnd  38503  heibor1lem  38518  isrngohom  38674  isidl  38723  isfldidl2  38778  isdmn3  38783  sbccom2lem  38831  scott0f  38876  triantru3  38943  vvdifopab  38972  brres2  38980  eldmqsres  39000  inxpss  39024  ref5  39026  n0el2  39042  dfsucmap3  39170  trcoss2  39281  dfeqvrel2  39381  dfeqvrel3  39382  redundeq1  39420  redundpbi1  39422  refrelredund4  39426  funALTVfun  39490  dfeldisj3  39518  dfeldisj5  39520  pet0  39625  petid  39627  petidres  39629  petinidres  39631  petxrnidres  39633  mpet  39660  petincnvepres  39670  pet  39672  pmapglbx  40601  lhpexle3  40844  cdleme25cv  41190  dicelval3  42012  diclspsn  42026  lcfls1c  42368  sn-axrep5v  43046  sn-iotalem  43050  psspwb  43057  redvmptabs  43179  eu6w  43466  moxfr  43481  fphpd  43601  uniel  44002  dflim6  44049  onsucf1olem  44055  dflim7  44058  omge2  44083  oenassex  44103  safesnsupfilb  44202  ifpim1  44253  ifpnot  44254  ifpid2  44255  ifpim2  44256  ifpxorcor  44260  ifpnot23  44262  ifpananb  44290  ifpnannanb  44291  ifpxorxorb  44295  rp-fakeinunass  44299  snen1g  44308  pren2  44337  alephiso2  44342  undmrnresiss  44388  cnvssco  44390  cotrintab  44398  cnviun  44434  imaiun1  44435  coiun1  44436  elintima  44437  frege133d  44549  frege54cor0a  44647  or3or  44807  andi3or  44808  ntrneik4w  44884  k0004lem1  44931  ismnuprim  45062  ismnushort  45069  undisjrab  45074  nzss  45085  pm10.541  45135  compab  45209  onfrALTlem5  45309  onfrALTlem5VD  45651  rext0  45705  wfaxun  45766  brpermmodel  45770  permaxrep  45773  permaxpow  45776  permac8prim  45781  eluni2f  45879  euabsneu  47823  aiotaexb  47884  aiotavb  47885  r19.32  47893  3an4ancom24  48064  ichn  48263  ichcom  48266  ichbi12i  48267  prproropf1olem0  48309  pairreueq  48317  clnbgrsym  48661  usgrexmpl2nb0  48854  usgrexmpl2nb1  48855  usgrexmpl2nb2  48856  usgrexmpl2nb3  48857  usgrexmpl2nb4  48858  usgrexmpl2nb5  48859  sgrp2sgrp  49050  isidom3  49167  islindeps  49290  elbigo  49388  reutruALT  49640  coxp  49668  tposres0  49712  catcinv  50234  isthincd2  50272  setrec1lem3  50524  elpg  50549  dfrals2  50625  alsbii  50635  ralsbii  50636  cbvals  50640  dfralseu2  50658  alseubii  50667  ralseubii  50668