Theorem bitr4i 278

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 224	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 275	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  3bitr2i  299  3bitr2ri  300  3bitr4i  303  3bitr4ri  304  biluk  385  biancomi  462  dfbi2  474  imdistan  567  pm5.32  573  bianass  642  mpbiran  709  biadaniALT  820  imor  853  imimorb  952  pm5.6  1003  nbi2  1017  casesifp  1077  3ancoma  1097  3ancomb  1098  3anrev  1100  dfnan2  1495  nannan  1498  nanbi  1501  xorcom  1515  xorneg  1524  xorbi12i  1525  norcom  1531  noran  1533  norasslem1  1535  trunortru  1590  trunorfal  1591  cadan  1610  cadcomb  1614  nic-ax  1674  nic-axALT  1675  nf3  1787  19.43  1883  equsv  2004  sbrimvw  2094  sbcom2  2176  sb5  2278  nf5  2284  nf6  2285  sbrim  2306  sbnf  2313  sb6x  2464  2sb5rf  2472  2sb6rf  2473  sb4b  2475  sb5f  2498  sbequ8  2501  sbhb  2521  eu6lem  2568  eu1  2605  iseqsetv-cleq  2795  issettru  2809  iseqsetv-clel  2810  issetlem  2811  cleqh  2860  cleqf  2923  sbabel  2927  necon3bii  2980  neor  3020  neorian  3023  rextru  3063  r19.26m  3091  r19.43  3100  3r19.43  3101  r2allem  3120  r19.23t  3228  ralcom4  3258  moel  3366  rabid2f  3426  eqv  3446  eqvf  3447  ralv  3463  rexv  3464  reuv  3465  rmov  3466  rexcom4b  3468  ceqsex4v  3493  ceqsex8v  3495  ceqsrexv  3610  rexab  3654  ralrab2  3657  rexrab2  3659  reu2  3684  reu3  3686  reueq  3696  2reuswap  3705  2reuswap2  3706  reuind  3712  2reu5lem3  3716  2rmoswap  3720  rmo2  3838  rmoanim  3845  rmoanimALT  3846  dfss3  3923  dfss3f  3926  ssabral  4016  rabss  4022  ssrabeq  4034  uniiunlem  4037  sspsstri  4055  npss  4063  dfdif3OLD  4068  raldifb  4099  uncom  4108  inass  4178  elsymdifxor  4210  nsspssun  4218  dfss4  4219  dfun2  4220  dfin2  4221  indi  4234  reupick3  4280  eq0f  4297  neq0f  4298  eq0  4300  eq0ALT  4301  dfnf5  4332  rabn0  4339  csbab  4390  vss  4396  disj  4400  disj3  4404  undisj1  4412  undisj2  4413  inundif  4429  undif  4432  undifr  4433  rabsssn  4621  exsnrex  4633  euabsn2  4678  euabsn  4679  raldifsni  4747  tppreqb  4757  pwpw0  4765  prssg  4771  ssunsn  4780  prneimg2  4807  preqsn  4814  pwpr  4853  dfuni2  4861  unissb  4891  elint2  4904  ssint  4914  uniintab  4936  dfiin2g  4981  iunid  5009  iunn0  5015  iunxun  5042  iunxiun  5045  iinpw  5054  disjor  5073  disjxiun  5088  dftr2  5200  dftr3  5203  dftr4  5204  axrep6OLD  5227  vnex  5252  inuni  5288  eusv2  5334  reusv2lem4  5339  rexxfr  5354  sspwb  5390  opthneg  5421  pwssun  5508  dfid3  5514  dffr6  5572  dffr2  5577  dffr2ALT  5578  opthprc  5680  elxp3  5682  xpiundir  5688  elvv  5691  reliun  5756  inxpOLD  5772  raliunxp  5779  cnvuni  5826  dmopab2rex  5857  dm0rn0OLD  5865  dfres3  5933  ssdmres  5962  elidinxp  5993  idinxpres  5996  dfima2  6011  args  6041  dffr3  6048  cotrg  6058  intasym  6062  asymref  6063  intirr  6065  xpnz  6106  xp11  6122  ssrnres  6125  xpimasn  6132  coiun  6204  coass  6213  cnvso  6235  elsnxp  6238  dfpo2  6243  imaindm  6246  dffr4  6267  dfse3  6283  frpoind  6289  dflim2  6364  orddif  6404  dffun6  6492  dffun6f  6496  dffun7  6508  dffun9  6510  funfn  6511  svrelfun  6553  mptfnf  6616  dffn2  6653  dffn3  6663  fint  6702  dffn4  6741  dff1o4  6771  brprcneu  6812  brprcneuALT  6813  eqfnfv3  6966  fnreseql  6981  fsn  7068  ftpg  7089  abrexco  7178  imaiun  7179  dff13  7188  isof1oidb  7258  isof1oopb  7259  isocnv2  7265  eloprabga  7455  mpo2eqb  7478  elovmpo  7591  sorpss  7661  abexex  7903  elxp6  7955  elxp7  7956  releldm2  7975  opiota  7991  fnmpo  8001  frxp  8056  frxp2  8074  soseq  8089  cnvimadfsn  8102  mpoxneldm  8142  dftpos4  8175  frrlem9  8224  dfrecs3  8292  tfrlem7  8302  ondif1  8416  oarec  8477  oeeu  8518  brinxper  8651  0er  8660  eroveu  8736  erovlem  8737  elixpconst  8829  domen  8884  brsdom  8897  brdom2  8904  reuen1  8948  sbthlem10  9009  brsdom2  9014  xpf1o  9052  unfi  9080  sbthfilem  9107  onfin2  9125  0sdom1domALT  9131  modom  9135  marypha2lem3  9321  wemapsolem  9436  elom3  9538  dfom5  9540  brttrcl2  9604  ttrcltr  9606  ttrclse  9617  trcl  9618  epfrs  9621  frind  9640  rankf  9684  scottexs  9777  scott0s  9778  cplem1  9779  hta  9787  djuexb  9799  pm54.43lem  9890  alephsuc2  9968  iscard3  9981  aceq0  10006  aceq3lem  10008  dfac3  10009  dfac5lem2  10012  dfac5  10017  dfac7  10021  dfac12a  10037  kmlem12  10050  kmlem14  10052  kmlem15  10053  infmap2  10105  ackbij2  10130  dfacfin7  10287  ituniiun  10310  zorng  10392  brdom7disj  10419  entri2  10446  alephreg  10470  fpwwe2lem11  10529  fpwwe2lem12  10530  pwfseqlem1  10546  grutsk  10710  axgroth4  10720  grothprim  10722  grothtsk  10723  elni2  10765  ltsopi  10776  genpass  10897  psslinpr  10919  ltexprlem4  10927  ltresr  11028  infm3  12078  elnnz  12475  dfz2  12484  2rexuz  12795  nnwos  12810  eluz2b1  12814  qexALT  12859  elxr  13012  dflt2  13044  xrsupss  13205  xrinfmss  13206  elixx1  13251  elioo2  13283  dfrp2  13291  elioopnf  13340  elicopnf  13342  elfz1  13409  fznn  13489  fzp1nel  13508  fznn0  13516  preduz  13547  prinfzo0  13595  injresinj  13688  nn0opthlem1  14172  faclbnd4lem1  14197  hashfxnn0  14241  hashprdifel  14302  hashgt23el  14328  hashfun  14341  hashf1  14361  fz1isolem  14365  f1oun2prg  14821  brtrclfv  14906  shftdm  14975  rediv  15035  imdiv  15042  rexanre  15251  caubnd  15263  climreu  15460  prodmo  15840  dvdslelem  16217  3dvdsdec  16240  3dvds2dec  16241  bitsval  16332  smueqlem  16398  algcvgblem  16485  lcmfunsnlem2  16548  isprm2  16590  isprm3  16591  isprm4  16592  pythagtriplem2  16726  elgz  16840  hashbc0  16914  0ram  16929  isstruct  17060  issect  17657  isfull2  17817  isfth2  17821  fucinv  17880  eldmcoa  17969  isdrs  18204  submacs  18732  isnsg4  19077  isgim  19172  gaorb  19217  oppgid  19266  oppgsubm  19272  oppgcntz  19274  ispgp  19502  efgsdm  19640  efgcpbllema  19664  iscyg2  19792  isomnd  20033  omndmul2  20043  isrng  20070  isring  20153  isirred2  20337  opprirred  20338  isrnghm  20357  dfrhm2  20390  isnzr2  20431  opprsubrng  20472  opprsubrg  20506  isdomn3  20628  drngid2  20665  issdrg  20701  islmod  20795  lss1d  20894  islmhm  20959  islmim  20994  lbsextlem2  21094  lidlnz  21177  dfprm2  21408  isphl  21563  elocv  21603  iunocv  21616  isobs  21655  islinds  21744  1mavmul  22461  toprntopon  22838  isbasis3g  22862  fctop  22917  cctop  22919  isclo2  23001  restsn  23083  lmbr  23171  ist0-3  23258  2ndcdisj  23369  1stccnp  23375  islocfin  23430  1stckgenlem  23466  txbas  23480  ptbasin  23490  tx2cn  23523  fbfinnfr  23754  fbasrn  23797  filuni  23798  ufinffr  23842  fin1aufil  23845  rnelfmlem  23865  flimrest  23896  alexsubALTlem3  23962  alexsubALTlem4  23963  tgphaus  24030  istlm  24098  iscusp2  24214  metuel2  24478  isngp2  24510  isnlm  24588  isphtpc  24918  phtpcer  24919  om1elbas  24957  isclm  24989  iscvsp  25053  iscph  25095  iscau3  25203  minveclem3b  25353  elovolm  25401  ioombl1lem4  25487  dyaddisj  25522  vitali  25539  itg1climres  25640  itg2seq  25668  itg2monolem1  25676  itg2mono  25679  limcrcl  25800  lhop1  25944  itgsubst  25981  mdegleb  25994  isuc1p  26071  ismon1p  26073  plydivex  26230  ellogdm  26573  1cubr  26777  atandm2  26812  birthdaylem3  26888  dmarea  26892  dchrelbas2  27173  dchrelbas4  27179  elno3  27592  nosgnn0  27595  nosepon  27602  nocvxminlem  27715  scutcut  27740  scutbday  27743  dmscut  27750  scutf  27751  sltrec  27760  made0  27816  addsprop  27917  negsproplem2  27969  negsprop  27975  mulsprop  28067  precsexlem10  28152  elzs2  28321  elnnzs  28323  recut  28396  0reno  28397  axcontlem7  28946  nb3grpr  29358  nb3grpr2  29359  upgrwlkcompim  29619  wlkson  29631  wlkonprop  29633  wksonproplem  29679  ispth  29697  wwlknon  29833  wwlksnextinj  29875  wspthsnwspthsnon  29892  elwspths2spth  29943  rusgrnumwwlkl1  29944  clwwlkccatlem  29964  erclwwlkref  29995  frgr3v  30250  nmoubi  30747  nmobndseqi  30754  nmobndseqiALT  30755  minvecolem1  30849  isch2  31198  hlimreui  31214  isch3  31216  ocsh  31258  dfch2  31382  spanuni  31519  nonbooli  31626  5oalem7  31635  adjsym  31808  elbdop2  31846  dmadjss  31862  nmopub  31883  nmfnleub  31900  nmop0h  31966  pjssposi  32147  pjordi  32148  cvbr2  32258  cvnbtwn2  32262  mdsl2i  32297  cvmdi  32299  elat2  32315  atom1d  32328  chirredi  32369  cdj3i  32416  or3di  32433  opreu2reu1  32458  mo5f  32463  reuxfrdf  32465  rexunirn  32466  difrab2  32472  rabsspr  32476  rabsstp  32477  tpssg  32512  iuninc  32535  disjorf  32554  disjunsn  32569  rabfmpunirn  32630  aciunf1  32640  funcnv5mpt  32645  eliccelico  32755  elicoelioo  32756  isslmd  33166  islinds5  33327  ismxidl  33422  1arithufdlem4  33507  hasheuni  34093  pwsiga  34138  sigainb  34144  issros  34183  2ndmbfm  34269  omssubaddlem  34307  omssubadd  34308  sitgaddlemb  34356  eulerpartlemgvv  34384  eulerpartlemn  34389  probun  34427  ballotlem2  34497  ballotlemodife  34506  bnj252  34710  bnj253  34711  bnj255  34712  bnj345  34721  bnj133  34734  bnj976  34784  bnj1098  34790  bnj121  34877  bnj130  34881  bnj150  34883  bnj581  34915  bnj607  34923  bnj865  34930  bnj917  34941  bnj934  34942  bnj964  34950  bnj983  34958  bnj996  34963  bnj1021  34973  bnj1033  34976  bnj1047  34980  bnj1049  34981  bnj1090  34986  bnj1128  34997  bnj1175  35011  bnj1189  35016  bnj1253  35024  bnj1312  35065  exdifsn  35086  fineqvrep  35125  fineqvac  35127  onvf1odlem4  35138  vonf1owev  35140  erdszelem9  35231  erdszelem10  35232  pconnconn  35263  cvmliftiota  35333  fmlaomn0  35422  fmla0disjsuc  35430  fmlasucdisj  35431  dmopab3rexdif  35437  elmthm  35608  antnestALT  35726  nepss  35750  xpab  35758  dfso2  35787  elrn3  35794  elpotr  35814  dfon2lem5  35820  dfon2lem7  35822  dfon2lem8  35823  elwlim  35856  wzel  35857  brtxp2  35914  brpprod3a  35919  eltrans  35924  dfon3  35925  dffix2  35938  dffun10  35947  elfuns  35948  brsingle  35950  brimg  35970  funpartfun  35976  funpartfv  35978  cgrxfr  36088  segletr  36147  outsideoftr  36162  neifg  36404  filnetlem4  36414  df3nandALT1  36432  weiunlem2  36496  bj-consensusALT  36612  bj-df-ifc  36613  bj-biexal3  36740  bj-nfnnfTEMP  36791  bj-denoteslem  36904  bj-denotesALTV  36905  bj-ralvw  36912  bj-rexvw  36913  bj-rexcom4bv  36915  bj-rexcom4b  36916  bj-sbeq  36934  bj-inrab  36960  bj-rcleqf  37058  bj-dfmpoa  37151  bj-imdirco  37223  topdifinffinlem  37380  topdifinfeq  37383  relowlssretop  37396  relowlpssretop  37397  rdgeqoa  37403  domalom  37437  nlpineqsn  37441  fvineqsneq  37445  wl-ifpimpr  37499  wl-df3xor3  37503  wl-3xorbi  37506  wl-3xorbi2  37507  wl-2xor  37516  wl-2mintru2  37524  wl-dfclab  37629  rabiun  37632  phpreu  37643  fin2solem  37645  matunitlindflem2  37656  ptrest  37658  poimirlem25  37684  poimirlem27  37686  poimirlem30  37689  ismblfin  37700  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  itg2addnclem2  37711  fdc  37784  prdstotbnd  37833  isdrngo1  37995  ispridl  38073  ismaxidl  38079  impor  38120  selconj  38139  tradd  38144  scott0f  38208  r2alan  38283  inxpss3  38347  idinxpssinxp2  38351  idinxpssinxp3  38352  dfrel5  38373  ineleq  38381  moantr  38391  dfxrn2  38403  inxpxrn  38426  rnxrnres  38430  coss1cnvres  38453  1cossres  38465  cocossss  38472  cossssid4  38506  cossssid5  38507  cosscnvssid5  38514  cossid  38516  dfssr2  38535  cnvrefrelcoss2  38573  cosselcnvrefrels2  38574  eqvrelcoss  38653  eqvrelcoss2  38655  dfcoeleqvrel  38658  refrelredund4  38671  cnvepresdmqs  38690  dfcomember  38709  dfdisjALTV  38750  dfeldisj3  38756  dfeldisj4  38757  dfeldisj5  38758  disjres  38781  prter1  38917  islshp  39017  islshpat  39055  lcvbr2  39060  lcvnbtwn2  39065  cvrnbtwn3  39314  isatl  39337  ishlat1  39390  ishlat2  39391  cvrat4  39481  pmapglbx  39807  lhpexle3  40050  dib1dim  41203  diblsmopel  41209  lcfls1lem  41572  prjsperref  42638  prjspeclsp  42644  euabsn2w  42711  rexrabdioph  42826  dford4  43061  onsupuni  43261  dflim6  43296  tfsconcatlem  43368  naddgeoa  43426  ifpdfor2  43493  ifpdfan2  43495  ifpdfor  43497  ifpdfan  43498  ifpnot23b  43514  ifpnot23c  43516  ifpnot23d  43517  ifpim123g  43532  ifpbibib  43542  clss2lem  43643  imaiun1  43683  coiun1  43684  brfvrcld2  43724  iunrelexp0  43734  brtrclfv2  43759  snhesn  43818  dffrege76  43971  frege97  43992  frege98  43993  frege109  44004  frege110  44005  dffrege115  44010  frege131  44026  frege133  44028  ntrneineine1lem  44116  ntrneiel2  44118  ntrneiiso  44123  gneispace3  44165  scotteld  44278  ismnuprim  44326  ismnushort  44333  dfuniv2  44334  pm11.52  44419  pm11.58  44422  pm13.192  44442  impexpdcom  44547  sbc3or  44564  opelopab4  44583  uunT12p1  44831  uunT12p2  44832  uunT12p3  44833  uun2221  44844  uun2221p1  44845  uun2221p2  44846  undif3VD  44913  modelaxreplem3  45012  permaxext  45037  permac8prim  45046  ndisj2  45087  nssrex  45122  rabssf  45155  bothtbothsame  46929  bothfbothsame  46930  aiffbtbat  46938  reuabaiotaiota  47117  2reu8i  47143  2reuimp0  47144  ichn  47486  dfodd2  47666  dfeven5  47696  dfodd7  47697  1nevenALTV  47721  oddprmne2  47745  dfvopnbgr2  47883  isuspgrim0lem  47923  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpg5edgnedg  48160  islindeps2  48514  isldepslvec2  48516  line2xlem  48784  rmotru  48833  reutru  48834  isnrm4  48961  iscnrm4  48984  homf0  49040  fuco2el  49343  isthincd2  49468  thinccic  49502  istermc2  49506  istermc3  49507  dftermc3  49562  setrec1lem3  49720  aacllem  49832