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  2096  sbcom2  2178  sb5  2280  nf5  2286  nf6  2287  sbrim  2308  sbnf  2315  sb6x  2466  2sb5rf  2474  2sb6rf  2475  sb4b  2477  sb5f  2500  sbequ8  2503  sbhb  2523  eu6lem  2570  eu1  2607  iseqsetv-cleq  2797  issettru  2811  iseqsetv-clel  2812  issetlem  2813  cleqh  2862  cleqf  2924  sbabel  2928  necon3bii  2981  neor  3021  neorian  3024  rextru  3064  r19.26m  3092  r19.43  3101  3r19.43  3102  r2allem  3121  r19.23t  3229  ralcom4  3259  moel  3367  rabid2f  3427  eqv  3447  eqvf  3448  ralv  3464  rexv  3465  reuv  3466  rmov  3467  rexcom4b  3469  ceqsex4v  3493  ceqsex8v  3495  ceqsrexv  3606  rexab  3650  ralrab2  3653  rexrab2  3655  reu2  3680  reu3  3682  reueq  3692  2reuswap  3701  2reuswap2  3702  reuind  3708  2reu5lem3  3712  2rmoswap  3716  rmo2  3834  rmoanim  3841  rmoanimALT  3842  dfss3  3919  dfss3f  3922  ssabral  4013  rabss  4019  ssrabeq  4033  uniiunlem  4036  sspsstri  4054  npss  4062  dfdif3OLD  4067  raldifb  4098  uncom  4107  inass  4177  elsymdifxor  4209  nsspssun  4217  dfss4  4218  dfun2  4219  dfin2  4220  indi  4233  reupick3  4279  eq0f  4296  neq0f  4297  eq0  4299  eq0ALT  4300  dfnf5  4331  rabn0  4338  csbab  4389  vss  4395  disj  4399  disj3  4403  undisj1  4411  undisj2  4412  inundif  4428  undif  4431  undifr  4432  rabsssn  4620  exsnrex  4632  euabsn2  4677  euabsn  4678  raldifsni  4746  tppreqb  4756  pwpw0  4764  prssg  4770  ssunsn  4779  prneimg2  4806  preqsn  4813  pwpr  4852  dfuni2  4860  unissb  4891  elint2  4904  ssint  4914  uniintab  4936  dfiin2g  4981  iunid  5011  iunn0  5017  iunxun  5044  iunxiun  5047  iinpw  5056  disjor  5075  disjxiun  5090  dftr2  5202  dftr3  5205  dftr4  5206  axrep6OLD  5229  vnex  5254  inuni  5290  eusv2  5336  reusv2lem4  5341  rexxfr  5356  sspwb  5392  opthneg  5424  pwssun  5511  dfid3  5517  dffr6  5575  dffr2  5580  dffr2ALT  5581  opthprc  5683  elxp3  5685  xpiundir  5691  elvv  5694  inxpOLD  5776  raliunxp  5783  cnvuni  5830  dmopab2rex  5861  dm0rn0OLD  5869  dfres3  5937  ssdmres  5966  elidinxp  5997  idinxpres  6000  dfima2  6015  args  6045  dffr3  6052  cotrg  6062  intasym  6066  asymref  6067  intirr  6069  xpnz  6111  xp11  6127  ssrnres  6130  xpimasn  6137  coiun  6209  coass  6218  cnvso  6240  elsnxp  6243  dfpo2  6248  imaindm  6251  dffr4  6272  dfse3  6288  frpoind  6294  dflim2  6369  orddif  6409  dffun6  6497  dffun6f  6501  dffun7  6513  dffun9  6515  funfn  6516  svrelfun  6558  mptfnf  6621  dffn2  6658  dffn3  6668  fint  6707  dffn4  6746  dff1o4  6776  brprcneu  6818  brprcneuALT  6819  eqfnfv3  6972  fnreseql  6987  fsn  7074  ftpg  7095  abrexco  7184  imaiun  7185  dff13  7194  isof1oidb  7264  isof1oopb  7265  isocnv2  7271  eloprabga  7461  mpo2eqb  7484  elovmpo  7597  sorpss  7667  abexex  7909  elxp6  7961  elxp7  7962  releldm2  7981  opiota  7997  fnmpo  8007  frxp  8062  frxp2  8080  soseq  8095  cnvimadfsn  8108  mpoxneldm  8148  dftpos4  8181  frrlem9  8230  dfrecs3  8298  tfrlem7  8308  ondif1  8422  oarec  8483  oeeu  8524  brinxper  8657  0er  8666  eroveu  8742  erovlem  8743  elixpconst  8835  domen  8890  brsdom  8903  brdom2  8911  reuen1  8955  sbthlem10  9016  brsdom2  9021  xpf1o  9059  unfi  9087  sbthfilem  9114  onfin2  9132  0sdom1domALT  9138  modom  9142  marypha2lem3  9328  wemapsolem  9443  elom3  9545  dfom5  9547  brttrcl2  9611  ttrcltr  9613  ttrclse  9624  trcl  9625  epfrs  9628  frind  9650  rankf  9694  scottexs  9787  scott0s  9788  cplem1  9789  hta  9797  djuexb  9809  pm54.43lem  9900  alephsuc2  9978  iscard3  9991  aceq0  10016  aceq3lem  10018  dfac3  10019  dfac5lem2  10022  dfac5  10027  dfac7  10031  dfac12a  10047  kmlem12  10060  kmlem14  10062  kmlem15  10063  infmap2  10115  ackbij2  10140  dfacfin7  10297  ituniiun  10320  zorng  10402  brdom7disj  10429  entri2  10456  alephreg  10480  fpwwe2lem11  10539  fpwwe2lem12  10540  pwfseqlem1  10556  grutsk  10720  axgroth4  10730  grothprim  10732  grothtsk  10733  elni2  10775  ltsopi  10786  genpass  10907  psslinpr  10929  ltexprlem4  10937  ltresr  11038  infm3  12088  elnnz  12485  dfz2  12494  2rexuz  12800  nnwos  12815  eluz2b1  12819  qexALT  12864  elxr  13017  dflt2  13049  xrsupss  13210  xrinfmss  13211  elixx1  13256  elioo2  13288  dfrp2  13296  elioopnf  13345  elicopnf  13347  elfz1  13414  fznn  13494  fzp1nel  13513  fznn0  13521  preduz  13552  prinfzo0  13600  injresinj  13693  nn0opthlem1  14177  faclbnd4lem1  14202  hashfxnn0  14246  hashprdifel  14307  hashgt23el  14333  hashfun  14346  hashf1  14366  fz1isolem  14370  f1oun2prg  14826  brtrclfv  14911  shftdm  14980  rediv  15040  imdiv  15047  rexanre  15256  caubnd  15268  climreu  15465  prodmo  15845  dvdslelem  16222  3dvdsdec  16245  3dvds2dec  16246  bitsval  16337  smueqlem  16403  algcvgblem  16490  lcmfunsnlem2  16553  isprm2  16595  isprm3  16596  isprm4  16597  pythagtriplem2  16731  elgz  16845  hashbc0  16919  0ram  16934  isstruct  17065  issect  17662  isfull2  17822  isfth2  17826  fucinv  17885  eldmcoa  17974  isdrs  18209  submacs  18737  isnsg4  19081  isgim  19176  gaorb  19221  oppgid  19270  oppgsubm  19276  oppgcntz  19278  ispgp  19506  efgsdm  19644  efgcpbllema  19668  iscyg2  19796  isomnd  20037  omndmul2  20047  isrng  20074  isring  20157  isirred2  20341  opprirred  20342  isrnghm  20361  dfrhm2  20394  isnzr2  20435  opprsubrng  20476  opprsubrg  20510  isdomn3  20632  drngid2  20669  issdrg  20705  islmod  20799  lss1d  20898  islmhm  20963  islmim  20998  lbsextlem2  21098  lidlnz  21181  dfprm2  21412  isphl  21567  elocv  21607  iunocv  21620  isobs  21659  islinds  21748  1mavmul  22464  toprntopon  22841  isbasis3g  22865  fctop  22920  cctop  22922  isclo2  23004  restsn  23086  lmbr  23174  ist0-3  23261  2ndcdisj  23372  1stccnp  23378  islocfin  23433  1stckgenlem  23469  txbas  23483  ptbasin  23493  tx2cn  23526  fbfinnfr  23757  fbasrn  23800  filuni  23801  ufinffr  23845  fin1aufil  23848  rnelfmlem  23868  flimrest  23899  alexsubALTlem3  23965  alexsubALTlem4  23966  tgphaus  24033  istlm  24101  iscusp2  24217  metuel2  24481  isngp2  24513  isnlm  24591  isphtpc  24921  phtpcer  24922  om1elbas  24960  isclm  24992  iscvsp  25056  iscph  25098  iscau3  25206  minveclem3b  25356  elovolm  25404  ioombl1lem4  25490  dyaddisj  25525  vitali  25542  itg1climres  25643  itg2seq  25671  itg2monolem1  25679  itg2mono  25682  limcrcl  25803  lhop1  25947  itgsubst  25984  mdegleb  25997  isuc1p  26074  ismon1p  26076  plydivex  26233  ellogdm  26576  1cubr  26780  atandm2  26815  birthdaylem3  26891  dmarea  26895  dchrelbas2  27176  dchrelbas4  27182  elno3  27595  nosgnn0  27598  nosepon  27605  nocvxminlem  27718  scutcut  27743  scutbday  27746  dmscut  27753  scutf  27754  sltrec  27763  made0  27819  addsprop  27920  negsproplem2  27972  negsprop  27978  mulsprop  28070  precsexlem10  28155  elzs2  28324  elnnzs  28326  recut  28399  0reno  28400  axcontlem7  28950  nb3grpr  29362  nb3grpr2  29363  upgrwlkcompim  29623  wlkson  29635  wlkonprop  29637  wksonproplem  29683  ispth  29701  wwlknon  29837  wwlksnextinj  29879  wspthsnwspthsnon  29896  elwspths2spth  29950  rusgrnumwwlkl1  29951  clwwlkccatlem  29971  erclwwlkref  30002  frgr3v  30257  nmoubi  30754  nmobndseqi  30761  nmobndseqiALT  30762  minvecolem1  30856  isch2  31205  hlimreui  31221  isch3  31223  ocsh  31265  dfch2  31389  spanuni  31526  nonbooli  31633  5oalem7  31642  adjsym  31815  elbdop2  31853  dmadjss  31869  nmopub  31890  nmfnleub  31907  nmop0h  31973  pjssposi  32154  pjordi  32155  cvbr2  32265  cvnbtwn2  32269  mdsl2i  32304  cvmdi  32306  elat2  32322  atom1d  32335  chirredi  32376  cdj3i  32423  or3di  32440  opreu2reu1  32465  mo5f  32470  reuxfrdf  32472  rexunirn  32473  difrab2  32479  rabsspr  32483  rabsstp  32484  tpssg  32519  iuninc  32542  disjorf  32561  disjunsn  32576  rabfmpunirn  32637  aciunf1  32647  funcnv5mpt  32652  eliccelico  32764  elicoelioo  32765  isslmd  33178  islinds5  33339  ismxidl  33434  1arithufdlem4  33519  hasheuni  34119  pwsiga  34164  sigainb  34170  issros  34209  2ndmbfm  34295  omssubaddlem  34333  omssubadd  34334  sitgaddlemb  34382  eulerpartlemgvv  34410  eulerpartlemn  34415  probun  34453  ballotlem2  34523  ballotlemodife  34532  bnj252  34736  bnj253  34737  bnj255  34738  bnj345  34747  bnj133  34760  bnj976  34810  bnj1098  34816  bnj121  34903  bnj130  34907  bnj150  34909  bnj581  34941  bnj607  34949  bnj865  34956  bnj917  34967  bnj934  34968  bnj964  34976  bnj983  34984  bnj996  34989  bnj1021  34999  bnj1033  35002  bnj1047  35006  bnj1049  35007  bnj1090  35012  bnj1128  35023  bnj1175  35037  bnj1189  35042  bnj1253  35050  bnj1312  35091  exdifsn  35112  fineqvrep  35158  fineqvac  35160  onvf1odlem4  35171  vonf1owev  35173  erdszelem9  35264  erdszelem10  35265  pconnconn  35296  cvmliftiota  35366  fmlaomn0  35455  fmla0disjsuc  35463  fmlasucdisj  35464  dmopab3rexdif  35470  elmthm  35641  antnestALT  35759  nepss  35783  xpab  35791  dfso2  35820  elrn3  35827  elpotr  35844  dfon2lem5  35850  dfon2lem7  35852  dfon2lem8  35853  elwlim  35886  wzel  35887  brtxp2  35944  brpprod3a  35949  eltrans  35954  dfon3  35955  dffix2  35968  dffun10  35977  elfuns  35978  brsingle  35980  brimg  36000  funpartfun  36008  funpartfv  36010  cgrxfr  36120  segletr  36179  outsideoftr  36194  neifg  36436  filnetlem4  36446  df3nandALT1  36464  weiunlem2  36528  bj-consensusALT  36644  bj-df-ifc  36645  bj-biexal3  36772  bj-nfnnfTEMP  36823  bj-denoteslem  36936  bj-denotesALTV  36937  bj-ralvw  36944  bj-rexvw  36945  bj-rexcom4bv  36947  bj-rexcom4b  36948  bj-sbeq  36966  bj-inrab  36992  bj-rcleqf  37090  bj-dfmpoa  37183  bj-imdirco  37255  topdifinffinlem  37412  topdifinfeq  37415  relowlssretop  37428  relowlpssretop  37429  rdgeqoa  37435  domalom  37469  nlpineqsn  37473  fvineqsneq  37477  wl-ifpimpr  37531  wl-df3xor3  37535  wl-3xorbi  37538  wl-3xorbi2  37539  wl-2xor  37548  wl-2mintru2  37556  wl-dfclab  37650  rabiun  37653  phpreu  37664  fin2solem  37666  matunitlindflem2  37677  ptrest  37679  poimirlem25  37705  poimirlem27  37707  poimirlem30  37710  ismblfin  37721  ovoliunnfl  37722  voliunnfl  37724  volsupnfl  37725  itg2addnclem2  37732  fdc  37805  prdstotbnd  37854  isdrngo1  38016  ispridl  38094  ismaxidl  38100  impor  38141  selconj  38160  tradd  38165  scott0f  38229  r2alan  38306  inxpss3  38372  idinxpssinxp2  38376  idinxpssinxp3  38377  dfrel5  38398  ineleq  38406  moantr  38416  dfxrn2  38429  inxpxrn  38462  rnxrnres  38466  dfsuccl4  38507  coss1cnvres  38539  1cossres  38551  cocossss  38558  cossssid4  38592  cossssid5  38593  cosscnvssid5  38600  cossid  38602  dfssr2  38611  cnvrefrelcoss2  38649  cosselcnvrefrels2  38650  eqvrelcoss  38733  eqvrelcoss2  38735  dfcoeleqvrel  38738  refrelredund4  38751  cnvepresdmqs  38771  dfcomember  38790  dfdisjALTV  38831  dfeldisj3  38837  dfeldisj4  38838  dfeldisj5  38839  disjres  38862  prter1  38998  islshp  39098  islshpat  39136  lcvbr2  39141  lcvnbtwn2  39146  cvrnbtwn3  39395  isatl  39418  ishlat1  39471  ishlat2  39472  cvrat4  39562  pmapglbx  39888  lhpexle3  40131  dib1dim  41284  diblsmopel  41290  lcfls1lem  41653  prjsperref  42724  prjspeclsp  42730  euabsn2w  42797  rexrabdioph  42911  dford4  43146  onsupuni  43346  dflim6  43381  tfsconcatlem  43453  naddgeoa  43511  ifpdfor2  43578  ifpdfan2  43580  ifpdfor  43582  ifpdfan  43583  ifpnot23b  43599  ifpnot23c  43601  ifpnot23d  43602  ifpim123g  43617  ifpbibib  43627  clss2lem  43728  imaiun1  43768  coiun1  43769  brfvrcld2  43809  iunrelexp0  43819  brtrclfv2  43844  snhesn  43903  dffrege76  44056  frege97  44077  frege98  44078  frege109  44089  frege110  44090  dffrege115  44095  frege131  44111  frege133  44113  ntrneineine1lem  44201  ntrneiel2  44203  ntrneiiso  44208  gneispace3  44250  scotteld  44363  ismnuprim  44411  ismnushort  44418  dfuniv2  44419  pm11.52  44504  pm11.58  44507  pm13.192  44527  impexpdcom  44632  sbc3or  44649  opelopab4  44668  uunT12p1  44916  uunT12p2  44917  uunT12p3  44918  uun2221  44929  uun2221p1  44930  uun2221p2  44931  undif3VD  44998  modelaxreplem3  45097  permaxext  45122  permac8prim  45131  ndisj2  45172  nssrex  45207  rabssf  45240  bothtbothsame  47023  bothfbothsame  47024  aiffbtbat  47032  reuabaiotaiota  47211  2reu8i  47237  2reuimp0  47238  ichn  47580  dfodd2  47760  dfeven5  47790  dfodd7  47791  1nevenALTV  47815  oddprmne2  47839  dfvopnbgr2  47977  isuspgrim0lem  48017  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpg5edgnedg  48254  islindeps2  48608  isldepslvec2  48610  line2xlem  48878  rmotru  48927  reutru  48928  isnrm4  49055  iscnrm4  49078  homf0  49134  fuco2el  49437  isthincd2  49562  thinccic  49596  istermc2  49600  istermc3  49601  dftermc3  49656  setrec1lem3  49814  aacllem  49926