Theorem bitr4i 280

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypotheses

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

Assertion

Ref	Expression
bitr4i	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitr4i

Step	Hyp	Ref	Expression
1		bitr4i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		bitr4i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	bicomi 226	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	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:  3bitr2i  301  3bitr2ri  302  3bitr4i  305  3bitr4ri  306  biluk  389  biancomi  465  dfbi2  477  imdistan  570  pm5.32  576  bianass  640  mpbiran  707  biadaniALT  819  imor  849  imimorb  947  pm5.6  998  nbi2  1012  casesifp  1071  3ancoma  1094  3ancomb  1095  3anrev  1097  an3andi  1478  nanimn  1484  nannan  1487  nanbi  1490  xorcom  1504  xorneg  1514  xorbi12i  1515  norcom  1522  noran  1526  norasslem1  1530  norassOLD  1534  trunortru  1586  trunorfal  1588  cadan  1610  cadcomb  1614  nic-ax  1674  nic-axALT  1675  nf3  1787  nfnbi  1855  19.43  1883  19.3vOLD  1989  equsv  2009  sb3an  2087  sbrimvlem  2101  sbcom2  2168  sb5OLD  2281  nf5  2290  nf6  2291  sb6x  2487  2sb5rf  2496  2sb6rf  2497  sb4b  2499  sb4bOLD  2500  sb5f  2538  sbequ8  2543  sbhb  2563  sb5ALT2  2586  sb5fALT  2603  eu6lem  2658  eu1  2694  cleqh  2936  clelab  2958  cleqf  3010  necon3bii  3068  neor  3108  neorian  3111  r19.26-3  3172  r19.26m  3173  r2allem  3200  r19.23t  3313  r19.43  3351  rexcom  3355  rabid2  3381  rabid2f  3382  eqv  3502  eqvf  3503  isset  3506  ralv  3519  rexv  3520  reuv  3521  rmov  3522  rexcom4b  3524  ceqsex4v  3546  ceqsex8v  3548  ceqsrexv  3649  ralrab2  3690  rexrab2  3693  reu2  3716  reu3  3718  reueq  3728  2reuswap  3737  2reuswap2  3738  reuind  3744  2reu5lem3  3748  2rmoswap  3752  sbc3an  3838  rmo2  3870  rmoanim  3878  rmoanimALT  3879  dfss2  3955  dfss3  3956  dfss3f  3959  ssabral  4042  rabss  4048  ssrabeq  4059  uniiunlem  4061  sspsstri  4079  npss  4087  dfdif3  4091  raldifb  4121  uncom  4129  inass  4196  elsymdifxor  4226  nsspssun  4234  dfss4  4235  dfun2  4236  dfin2  4237  indi  4250  indifdir  4260  difin2  4266  reupick3  4288  eq0f  4305  neq0f  4306  dfnf5  4334  rabn0  4339  csbab  4389  vss  4395  disj  4399  disj3  4403  undisj1  4411  undisj2  4412  inundif  4427  undif  4430  absn  4585  rabsssn  4607  exsnrex  4618  euabsn2  4661  euabsn  4662  raldifsni  4728  tppreqb  4738  pwpw0  4746  prssg  4752  ssunsn  4761  preqsn  4792  pwpr  4832  dfuni2  4840  unissb  4870  elint2  4883  ssint  4892  uniintab  4914  dfiin2g  4957  iunn0  4989  iunxun  5016  iunxiun  5019  iinpw  5028  disjor  5046  disjxiun  5063  dftr2  5174  dftr5  5175  dftr3  5176  dftr4  5177  axrep6  5197  vnex  5218  inuni  5246  eusv2  5297  reusv2lem4  5302  rexxfr  5317  snelpw  5338  sspwb  5342  opthneg  5373  pwssun  5456  dfid3  5462  dffr2  5520  opthprc  5616  elxp3  5618  xpiundir  5623  elvv  5626  reliun  5689  inxp  5703  raliunxp  5710  cnvuni  5757  dmopab2rex  5786  dm0rn0  5795  elrn  5822  dfres3  5858  ssdmres  5876  elidinxp  5911  idinxpres  5914  dfima2  5931  args  5957  dffr3  5962  cotrg  5971  intasym  5975  asymref  5976  intirr  5978  xpnz  6016  xp11  6032  ssrnres  6035  xpimasn  6042  coiun  6109  coass  6118  cnvso  6139  elsnxp  6142  dffr4  6164  wfi  6181  dflim2  6247  orddif  6284  dffun2  6365  dffun6f  6369  dffun7  6382  dffun9  6384  funfn  6385  svrelfun  6426  mptfnf  6483  dffn2  6516  dffn3  6525  fint  6558  dffn4  6596  dff1o4  6623  brprcneu  6662  eqfnfv3  6804  fnreseql  6818  fsn  6897  ftpg  6918  abrexco  7003  imaiun  7004  dff13  7013  isof1oidb  7077  isof1oopb  7078  isocnv2  7084  mpo2eqb  7283  elovmpo  7390  sorpss  7454  abexex  7672  elxp6  7723  elxp7  7724  releldm2  7742  opiota  7757  fnmpo  7767  frxp  7820  cnvimadfsn  7839  mpoxneldm  7878  dftpos4  7911  wfrlem8  7962  wfrfun  7965  dfrecs3  8009  tfrlem7  8019  ondif1  8126  oarec  8188  oeeu  8229  0er  8326  eroveu  8392  erovlem  8393  elixpconst  8469  domen  8522  brsdom  8532  brdom2  8539  reuen1  8578  sbthlem10  8636  brsdom2  8641  xpf1o  8679  onfin2  8710  0sdom1dom  8716  modom  8719  unfi  8785  marypha2lem3  8901  wemapsolem  9014  elom3  9111  dfom5  9113  trcl  9170  epfrs  9173  rankf  9223  scottexs  9316  scott0s  9317  cplem1  9318  karden  9324  hta  9326  djuexb  9338  pm54.43lem  9428  alephsuc2  9506  iscard3  9519  aceq0  9544  aceq3lem  9546  dfac3  9547  dfac5lem2  9550  dfac5  9554  dfac7  9558  dfac12a  9574  kmlem12  9587  kmlem14  9589  kmlem15  9590  infmap2  9640  ackbij2  9665  dfacfin7  9821  ituniiun  9844  zorng  9926  brdom7disj  9953  entri2  9980  alephreg  10004  fpwwe2lem12  10063  fpwwe2lem13  10064  pwfseqlem1  10080  grutsk  10244  axgroth4  10254  grothprim  10256  grothtsk  10257  elni2  10299  ltsopi  10310  genpass  10431  psslinpr  10453  ltexprlem4  10461  ltresr  10562  1re  10641  infm3  11600  elnnz  11992  dfz2  12001  2rexuz  12301  nnwos  12316  eluz2b1  12320  qexALT  12364  elxr  12512  dflt2  12542  xrsupss  12703  xrinfmss  12704  elixx1  12748  elioo2  12780  elioopnf  12832  elicopnf  12834  elfz1  12898  fznn  12976  fzp1nel  12992  fznn0  13000  preduz  13030  prinfzo0  13077  injresinj  13159  nn0opthlem1  13629  faclbnd4lem1  13654  hashfxnn0  13698  hashprdifel  13760  hashgt23el  13786  hashfun  13799  hashf1  13816  fz1isolem  13820  f1oun2prg  14279  brtrclfv  14362  shftdm  14430  rediv  14490  imdiv  14497  rexanre  14706  caubnd  14718  climreu  14913  prodmo  15290  dvdslelem  15659  3dvdsdec  15681  3dvds2dec  15682  bitsval  15773  smueqlem  15839  algcvgblem  15921  lcmfunsnlem2  15984  isprm2  16026  isprm3  16027  isprm4  16028  pythagtriplem2  16154  elgz  16267  hashbc0  16341  0ram  16356  isstruct  16496  issect  17023  isfull2  17181  isfth2  17185  fucinv  17243  eldmcoa  17325  isdrs  17544  submacs  17991  isnsg4  18319  isgim  18402  gaorb  18437  oppgid  18484  oppgsubm  18490  oppgcntz  18492  ispgp  18717  efgsdm  18856  efgcpbllema  18880  iscyg2  19001  isring  19301  isirred2  19451  opprirred  19452  dfrhm2  19469  drngid2  19518  opprsubrg  19556  issdrg  19574  islmod  19638  lss1d  19735  islmhm  19799  islmim  19834  lbsextlem2  19931  lidlnz  20001  isnzr2  20036  isassa  20088  dfprm2  20641  isphl  20772  elocv  20812  iunocv  20825  isobs  20864  islinds  20953  1mavmul  21157  toprntopon  21533  isbasis3g  21557  fctop  21612  cctop  21614  isclo2  21696  restsn  21778  lmbr  21866  ist0-3  21953  2ndcdisj  22064  1stccnp  22070  islocfin  22125  1stckgenlem  22161  txbas  22175  ptbasin  22185  tx2cn  22218  fbfinnfr  22449  fbasrn  22492  filuni  22493  ufinffr  22537  fin1aufil  22540  rnelfmlem  22560  flimrest  22591  alexsubALTlem3  22657  alexsubALTlem4  22658  tgphaus  22725  istlm  22793  iscusp2  22911  metuel2  23175  isngp2  23206  isnlm  23284  isphtpc  23598  phtpcer  23599  om1elbas  23636  isclm  23668  iscvsp  23732  iscph  23774  iscau3  23881  minveclem3b  24031  elovolm  24076  ioombl1lem4  24162  dyaddisj  24197  vitali  24214  itg1climres  24315  itg2seq  24343  itg2monolem1  24351  itg2mono  24354  limcrcl  24472  lhop1  24611  itgsubst  24646  mdegleb  24658  isuc1p  24734  ismon1p  24736  plydivex  24886  ellogdm  25222  1cubr  25420  atandm2  25455  birthdaylem3  25531  dmarea  25535  dchrelbas2  25813  dchrelbas4  25819  axcontlem7  26756  nb3grpr  27164  nb3grpr2  27165  upgrwlkcompim  27424  wlkson  27438  wlkonprop  27440  wksonproplem  27486  ispth  27504  wwlknon  27635  wwlksnextinj  27677  wspthsnwspthsnon  27695  elwspths2spth  27746  rusgrnumwwlkl1  27747  clwwlkccatlem  27767  erclwwlkref  27798  frgr3v  28054  nmoubi  28549  nmobndseqi  28556  nmobndseqiALT  28557  minvecolem1  28651  isch2  29000  hlimreui  29016  isch3  29018  ocsh  29060  dfch2  29184  spanuni  29321  nonbooli  29428  5oalem7  29437  adjsym  29610  elbdop2  29648  dmadjss  29664  nmopub  29685  nmfnleub  29702  nmop0h  29768  pjssposi  29949  pjordi  29950  cvbr2  30060  cvnbtwn2  30064  mdsl2i  30099  cvmdi  30101  elat2  30117  atom1d  30130  chirredi  30171  cdj3i  30218  or3di  30225  opreu2reu1  30247  moel  30252  mo5f  30253  reuxfrdf  30255  rexunirn  30256  difrab2  30261  iuninc  30312  disjorf  30329  disjunsn  30344  rabfmpunirn  30398  aciunf1  30408  funcnv5mpt  30413  dfrp2  30491  eliccelico  30500  elicoelioo  30501  isomnd  30702  omndmul2  30713  isslmd  30830  islinds5  30932  ismxidl  30971  hasheuni  31344  pwsiga  31389  sigainb  31395  issros  31434  2ndmbfm  31519  omssubaddlem  31557  omssubadd  31558  sitgaddlemb  31606  eulerpartlemgvv  31634  eulerpartlemn  31639  probun  31677  ballotlem2  31746  ballotlemodife  31755  bnj252  31973  bnj253  31974  bnj255  31975  bnj345  31984  bnj133  31997  bnj976  32049  bnj1098  32055  bnj121  32142  bnj130  32146  bnj150  32148  bnj581  32180  bnj607  32188  bnj865  32195  bnj917  32206  bnj934  32207  bnj964  32215  bnj983  32223  bnj996  32228  bnj1021  32238  bnj1033  32241  bnj1047  32245  bnj1049  32246  bnj1090  32251  bnj1128  32262  bnj1175  32276  bnj1189  32281  bnj1253  32289  bnj1312  32330  exdifsn  32345  erdszelem9  32446  erdszelem10  32447  pconnconn  32478  cvmliftiota  32548  fmlaomn0  32637  fmla0disjsuc  32645  fmlasucdisj  32646  dmopab3rexdif  32652  elmthm  32823  nepss  32948  dfso2  32990  dfpo2  32991  elrn3  32998  imaindm  33022  elpotr  33026  dfon2lem5  33032  dfon2lem7  33034  dfon2lem8  33035  frpoind  33080  frind  33085  soseq  33096  elwlim  33110  wzel  33111  frrlem9  33131  elno3  33162  nosgnn0  33165  nosepon  33172  nocvxminlem  33247  scutcut  33266  scutbday  33267  dmscut  33272  scutf  33273  sltrec  33278  brtxp2  33342  brpprod3a  33347  eltrans  33352  dfon3  33353  dffix2  33366  dffun10  33375  elfuns  33376  brsingle  33378  brimg  33398  funpartfun  33404  funpartfv  33406  cgrxfr  33516  segletr  33575  outsideoftr  33590  neifg  33719  filnetlem4  33729  df3nandALT1  33747  bj-consensusALT  33912  bj-df-ifc  33913  bj-biexal3  34041  bj-nfnnfTEMP  34087  bj-denoteslem  34188  bj-denotes  34189  bj-ralvw  34198  bj-rexvw  34199  bj-rexcom4bv  34201  bj-rexcom4b  34202  bj-sbeq  34221  bj-inrab  34248  bj-rcleqf  34340  bj-dfmpoa  34413  topdifinffinlem  34631  topdifinfeq  34634  relowlssretop  34647  relowlpssretop  34648  rdgeqoa  34654  domalom  34688  nlpineqsn  34692  fvineqsneq  34696  wl-ifpdfbi  34749  wl-hadassbi  34750  wl-hadbi  34751  wl-dfclab  34843  wl-dfralsb  34852  wl-dfrexsb  34866  wl-dfrmosb  34868  wl-dfrmov  34869  wl-dfrabv  34877  rabiun  34880  phpreu  34891  fin2solem  34893  matunitlindflem2  34904  ptrest  34906  poimirlem25  34932  poimirlem27  34934  poimirlem30  34937  ismblfin  34948  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  itg2addnclem2  34959  fdc  35035  prdstotbnd  35087  isdrngo1  35249  ispridl  35327  ismaxidl  35333  impor  35374  selconj  35393  tradd  35398  scott0f  35462  inxpss3  35586  idinxpssinxp2  35590  idinxpssinxp3  35591  dfrel5  35618  ineleq  35623  moantr  35631  dfxrn2  35643  inxpxrn  35658  rnxrnres  35662  1cossres  35689  cocossss  35696  cossssid4  35725  cossssid5  35726  cosscnvssid5  35733  cossid  35735  dfssr2  35754  cnvrefrelcoss2  35788  cosselcnvrefrels2  35789  eqvrelcoss  35867  eqvrelcoss2  35869  dfcoeleqvrel  35872  refrelredund4  35885  cnvepresdmqs  35902  dfmember  35921  dfdisjALTV  35961  dfeldisj3  35967  dfeldisj4  35968  dfeldisj5  35969  prter1  36030  islshp  36130  islshpat  36168  lcvbr2  36173  lcvnbtwn2  36178  cvrnbtwn3  36427  isatl  36450  ishlat1  36503  ishlat2  36504  cvrat4  36594  pmapglbx  36920  lhpexle3  37163  dib1dim  38316  diblsmopel  38322  lcfls1lem  38685  prjsperref  39305  prjspeclsp  39311  rexrabdioph  39440  dford4  39675  isdomn3  39853  ifpdfor2  39875  ifpdfan2  39877  ifpdfor  39879  ifpdfan  39880  ifpdfbi  39888  ifpnot23b  39897  ifpnot23c  39899  ifpnot23d  39900  ifpim123g  39915  ifpbibib  39925  clss2lem  40020  imaiun1  40045  coiun1  40046  brfvrcld2  40086  iunrelexp0  40096  brtrclfv2  40121  snhesn  40181  dffrege76  40334  frege97  40355  frege98  40356  frege109  40367  frege110  40368  dffrege115  40373  frege131  40389  frege133  40391  ntrneineine1lem  40483  ntrneiel2  40485  ntrneiiso  40490  gneispace3  40532  scotteld  40631  ismnuprim  40679  pm11.52  40768  pm11.58  40771  pm13.192  40791  impexpdcom  40898  sbc3or  40915  opelopab4  40934  uunT12p1  41183  uunT12p2  41184  uunT12p3  41185  uun2221  41196  uun2221p1  41197  uun2221p2  41198  undif3VD  41265  ndisj2  41362  nssrex  41400  rabssf  41434  bothtbothsame  43184  bothfbothsame  43185  aiffbtbat  43193  reuabaiotaiota  43336  2reu8i  43361  2reuimp0  43362  ichn  43675  dfodd2  43850  dfeven5  43880  dfodd7  43881  1nevenALTV  43905  oddprmne2  43929  isrng  44196  isrnghm  44212  islindeps2  44587  isldepslvec2  44589  line2xlem  44789  setrec1lem3  44841  aacllem  44951