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  1494  nannan  1497  nanbi  1500  xorcom  1514  xorneg  1523  xorbi12i  1524  norcom  1530  noran  1532  norasslem1  1534  trunortru  1589  trunorfal  1590  cadan  1609  cadcomb  1613  nic-ax  1673  nic-axALT  1674  nf3  1786  19.43  1882  equsv  2003  sbrimvw  2092  sbcom2  2174  sb5  2276  nf5  2282  nf6  2283  sbrim  2304  sbnf  2311  sb6x  2462  2sb5rf  2470  2sb6rf  2471  sb4b  2473  sb5f  2496  sbequ8  2499  sbhb  2519  eu6lem  2566  eu1  2603  iseqsetv-cleq  2793  issettru  2806  iseqsetv-clel  2807  issetlem  2808  cleqh  2857  cleqf  2920  sbabel  2924  necon3bii  2977  neor  3017  neorian  3020  rextru  3060  r19.26m  3088  r19.43  3097  3r19.43  3098  r2allem  3117  r19.23t  3225  ralcom4  3255  moel  3365  rabid2f  3426  eqv  3446  eqvf  3447  ralv  3463  rexv  3464  reuv  3465  rmov  3466  rexcom4b  3468  ceqsex4v  3493  ceqsex8v  3495  ceqsrexv  3610  rexab  3655  ralrab2  3658  rexrab2  3660  reu2  3685  reu3  3687  reueq  3697  2reuswap  3706  2reuswap2  3707  reuind  3713  2reu5lem3  3717  2rmoswap  3721  rmo2  3839  rmoanim  3846  rmoanimALT  3847  dfss3  3924  dfss3f  3927  ssabral  4017  rabss  4023  ssrabeq  4035  uniiunlem  4038  sspsstri  4056  npss  4064  dfdif3OLD  4069  raldifb  4100  uncom  4109  inass  4179  elsymdifxor  4211  nsspssun  4219  dfss4  4220  dfun2  4221  dfin2  4222  indi  4235  reupick3  4281  eq0f  4298  neq0f  4299  eq0  4301  eq0ALT  4302  dfnf5  4333  rabn0  4340  csbab  4391  vss  4397  disj  4401  disj3  4405  undisj1  4413  undisj2  4414  inundif  4430  undif  4433  undifr  4434  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  4890  elint2  4903  ssint  4914  uniintab  4936  dfiin2g  4981  iunid  5009  iunn0  5016  iunxun  5043  iunxiun  5046  iinpw  5055  disjor  5074  disjxiun  5089  dftr2  5201  dftr3  5204  dftr4  5205  axrep6OLD  5228  vnex  5253  inuni  5289  eusv2  5335  reusv2lem4  5340  rexxfr  5355  sspwb  5392  opthneg  5424  pwssun  5511  dfid3  5517  dffr6  5575  dffr2  5580  dffr2ALT  5581  opthprc  5683  elxp3  5685  xpiundir  5691  elvv  5694  reliun  5759  inxpOLD  5775  raliunxp  5782  cnvuni  5829  dmopab2rex  5860  dm0rn0  5867  dfres3  5935  ssdmres  5964  elidinxp  5995  idinxpres  5998  dfima2  6013  args  6043  dffr3  6050  cotrg  6060  intasym  6064  asymref  6065  intirr  6067  xpnz  6108  xp11  6124  ssrnres  6127  xpimasn  6134  coiun  6205  coass  6214  cnvso  6236  elsnxp  6239  dfpo2  6244  imaindm  6247  dffr4  6268  dfse3  6284  frpoind  6290  dflim2  6365  orddif  6405  dffun6  6493  dffun6f  6497  dffun7  6509  dffun9  6511  funfn  6512  svrelfun  6554  mptfnf  6617  dffn2  6654  dffn3  6664  fint  6703  dffn4  6742  dff1o4  6772  brprcneu  6812  brprcneuALT  6813  eqfnfv3  6967  fnreseql  6982  fsn  7069  ftpg  7090  abrexco  7180  imaiun  7181  dff13  7191  isof1oidb  7261  isof1oopb  7262  isocnv2  7268  eloprabga  7458  mpo2eqb  7481  elovmpo  7594  sorpss  7664  abexex  7906  elxp6  7958  elxp7  7959  releldm2  7978  opiota  7994  fnmpo  8004  frxp  8059  frxp2  8077  soseq  8092  cnvimadfsn  8105  mpoxneldm  8145  dftpos4  8178  frrlem9  8227  dfrecs3  8295  tfrlem7  8305  ondif1  8419  oarec  8480  oeeu  8521  brinxper  8654  0er  8663  eroveu  8739  erovlem  8740  elixpconst  8832  domen  8887  brsdom  8900  brdom2  8907  reuen1  8951  sbthlem10  9013  brsdom2  9018  xpf1o  9056  unfi  9085  sbthfilem  9112  onfin2  9130  0sdom1domALT  9136  modom  9140  marypha2lem3  9327  wemapsolem  9442  elom3  9544  dfom5  9546  brttrcl2  9610  ttrcltr  9612  ttrclse  9623  trcl  9624  epfrs  9627  frind  9646  rankf  9690  scottexs  9783  scott0s  9784  cplem1  9785  hta  9793  djuexb  9805  pm54.43lem  9896  alephsuc2  9974  iscard3  9987  aceq0  10012  aceq3lem  10014  dfac3  10015  dfac5lem2  10018  dfac5  10023  dfac7  10027  dfac12a  10043  kmlem12  10056  kmlem14  10058  kmlem15  10059  infmap2  10111  ackbij2  10136  dfacfin7  10293  ituniiun  10316  zorng  10398  brdom7disj  10425  entri2  10452  alephreg  10476  fpwwe2lem11  10535  fpwwe2lem12  10536  pwfseqlem1  10552  grutsk  10716  axgroth4  10726  grothprim  10728  grothtsk  10729  elni2  10771  ltsopi  10782  genpass  10903  psslinpr  10925  ltexprlem4  10933  ltresr  11034  infm3  12084  elnnz  12481  dfz2  12490  2rexuz  12801  nnwos  12816  eluz2b1  12820  qexALT  12865  elxr  13018  dflt2  13050  xrsupss  13211  xrinfmss  13212  elixx1  13257  elioo2  13289  dfrp2  13297  elioopnf  13346  elicopnf  13348  elfz1  13415  fznn  13495  fzp1nel  13514  fznn0  13522  preduz  13553  prinfzo0  13601  injresinj  13691  nn0opthlem1  14175  faclbnd4lem1  14200  hashfxnn0  14244  hashprdifel  14305  hashgt23el  14331  hashfun  14344  hashf1  14364  fz1isolem  14368  f1oun2prg  14824  brtrclfv  14909  shftdm  14978  rediv  15038  imdiv  15045  rexanre  15254  caubnd  15266  climreu  15463  prodmo  15843  dvdslelem  16220  3dvdsdec  16243  3dvds2dec  16244  bitsval  16335  smueqlem  16401  algcvgblem  16488  lcmfunsnlem2  16551  isprm2  16593  isprm3  16594  isprm4  16595  pythagtriplem2  16729  elgz  16843  hashbc0  16917  0ram  16932  isstruct  17063  issect  17660  isfull2  17820  isfth2  17824  fucinv  17883  eldmcoa  17972  isdrs  18207  submacs  18701  isnsg4  19046  isgim  19141  gaorb  19186  oppgid  19235  oppgsubm  19241  oppgcntz  19243  ispgp  19471  efgsdm  19609  efgcpbllema  19633  iscyg2  19761  isomnd  20002  omndmul2  20012  isrng  20039  isring  20122  isirred2  20306  opprirred  20307  isrnghm  20326  dfrhm2  20359  isnzr2  20403  opprsubrng  20444  opprsubrg  20478  isdomn3  20600  drngid2  20637  issdrg  20673  islmod  20767  lss1d  20866  islmhm  20931  islmim  20966  lbsextlem2  21066  lidlnz  21149  dfprm2  21380  isphl  21535  elocv  21575  iunocv  21588  isobs  21627  islinds  21716  1mavmul  22433  toprntopon  22810  isbasis3g  22834  fctop  22889  cctop  22891  isclo2  22973  restsn  23055  lmbr  23143  ist0-3  23230  2ndcdisj  23341  1stccnp  23347  islocfin  23402  1stckgenlem  23438  txbas  23452  ptbasin  23462  tx2cn  23495  fbfinnfr  23726  fbasrn  23769  filuni  23770  ufinffr  23814  fin1aufil  23817  rnelfmlem  23837  flimrest  23868  alexsubALTlem3  23934  alexsubALTlem4  23935  tgphaus  24002  istlm  24070  iscusp2  24187  metuel2  24451  isngp2  24483  isnlm  24561  isphtpc  24891  phtpcer  24892  om1elbas  24930  isclm  24962  iscvsp  25026  iscph  25068  iscau3  25176  minveclem3b  25326  elovolm  25374  ioombl1lem4  25460  dyaddisj  25495  vitali  25512  itg1climres  25613  itg2seq  25641  itg2monolem1  25649  itg2mono  25652  limcrcl  25773  lhop1  25917  itgsubst  25954  mdegleb  25967  isuc1p  26044  ismon1p  26046  plydivex  26203  ellogdm  26546  1cubr  26750  atandm2  26785  birthdaylem3  26861  dmarea  26865  dchrelbas2  27146  dchrelbas4  27152  elno3  27565  nosgnn0  27568  nosepon  27575  nocvxminlem  27688  scutcut  27713  scutbday  27716  dmscut  27723  scutf  27724  sltrec  27733  made0  27789  addsprop  27890  negsproplem2  27942  negsprop  27948  mulsprop  28040  precsexlem10  28125  elzs2  28294  elnnzs  28296  recut  28369  0reno  28370  axcontlem7  28919  nb3grpr  29331  nb3grpr2  29332  upgrwlkcompim  29592  wlkson  29604  wlkonprop  29606  wksonproplem  29652  ispth  29670  wwlknon  29806  wwlksnextinj  29848  wspthsnwspthsnon  29865  elwspths2spth  29916  rusgrnumwwlkl1  29917  clwwlkccatlem  29937  erclwwlkref  29968  frgr3v  30223  nmoubi  30720  nmobndseqi  30727  nmobndseqiALT  30728  minvecolem1  30822  isch2  31171  hlimreui  31187  isch3  31189  ocsh  31231  dfch2  31355  spanuni  31492  nonbooli  31599  5oalem7  31608  adjsym  31781  elbdop2  31819  dmadjss  31835  nmopub  31856  nmfnleub  31873  nmop0h  31939  pjssposi  32120  pjordi  32121  cvbr2  32231  cvnbtwn2  32235  mdsl2i  32270  cvmdi  32272  elat2  32288  atom1d  32301  chirredi  32342  cdj3i  32389  or3di  32407  opreu2reu1  32432  mo5f  32437  reuxfrdf  32439  rexunirn  32440  difrab2  32446  rabsspr  32450  rabsstp  32451  tpssg  32486  iuninc  32509  disjorf  32528  disjunsn  32543  rabfmpunirn  32604  aciunf1  32614  funcnv5mpt  32619  eliccelico  32729  elicoelioo  32730  isslmd  33153  islinds5  33313  ismxidl  33408  1arithufdlem4  33493  hasheuni  34068  pwsiga  34113  sigainb  34119  issros  34158  2ndmbfm  34245  omssubaddlem  34283  omssubadd  34284  sitgaddlemb  34332  eulerpartlemgvv  34360  eulerpartlemn  34365  probun  34403  ballotlem2  34473  ballotlemodife  34482  bnj252  34686  bnj253  34687  bnj255  34688  bnj345  34697  bnj133  34710  bnj976  34760  bnj1098  34766  bnj121  34853  bnj130  34857  bnj150  34859  bnj581  34891  bnj607  34899  bnj865  34906  bnj917  34917  bnj934  34918  bnj964  34926  bnj983  34934  bnj996  34939  bnj1021  34949  bnj1033  34952  bnj1047  34956  bnj1049  34957  bnj1090  34962  bnj1128  34973  bnj1175  34987  bnj1189  34992  bnj1253  35000  bnj1312  35041  exdifsn  35062  fineqvrep  35086  fineqvac  35088  onvf1odlem4  35099  vonf1owev  35101  erdszelem9  35192  erdszelem10  35193  pconnconn  35224  cvmliftiota  35294  fmlaomn0  35383  fmla0disjsuc  35391  fmlasucdisj  35392  dmopab3rexdif  35398  elmthm  35569  antnestALT  35687  nepss  35711  xpab  35719  dfso2  35748  elrn3  35755  elpotr  35775  dfon2lem5  35781  dfon2lem7  35783  dfon2lem8  35784  elwlim  35817  wzel  35818  brtxp2  35875  brpprod3a  35880  eltrans  35885  dfon3  35886  dffix2  35899  dffun10  35908  elfuns  35909  brsingle  35911  brimg  35931  funpartfun  35937  funpartfv  35939  cgrxfr  36049  segletr  36108  outsideoftr  36123  neifg  36365  filnetlem4  36375  df3nandALT1  36393  weiunlem2  36457  bj-consensusALT  36573  bj-df-ifc  36574  bj-biexal3  36701  bj-nfnnfTEMP  36752  bj-denoteslem  36865  bj-denotesALTV  36866  bj-ralvw  36873  bj-rexvw  36874  bj-rexcom4bv  36876  bj-rexcom4b  36877  bj-sbeq  36895  bj-inrab  36921  bj-rcleqf  37019  bj-dfmpoa  37112  bj-imdirco  37184  topdifinffinlem  37341  topdifinfeq  37344  relowlssretop  37357  relowlpssretop  37358  rdgeqoa  37364  domalom  37398  nlpineqsn  37402  fvineqsneq  37406  wl-ifpimpr  37460  wl-df3xor3  37464  wl-3xorbi  37467  wl-3xorbi2  37468  wl-2xor  37477  wl-2mintru2  37485  wl-dfclab  37590  rabiun  37593  phpreu  37604  fin2solem  37606  matunitlindflem2  37617  ptrest  37619  poimirlem25  37645  poimirlem27  37647  poimirlem30  37650  ismblfin  37661  ovoliunnfl  37662  voliunnfl  37664  volsupnfl  37665  itg2addnclem2  37672  fdc  37745  prdstotbnd  37794  isdrngo1  37956  ispridl  38034  ismaxidl  38040  impor  38081  selconj  38100  tradd  38105  scott0f  38169  r2alan  38244  inxpss3  38308  idinxpssinxp2  38312  idinxpssinxp3  38313  dfrel5  38334  ineleq  38342  moantr  38352  dfxrn2  38364  inxpxrn  38387  rnxrnres  38391  coss1cnvres  38414  1cossres  38426  cocossss  38433  cossssid4  38467  cossssid5  38468  cosscnvssid5  38475  cossid  38477  dfssr2  38496  cnvrefrelcoss2  38534  cosselcnvrefrels2  38535  eqvrelcoss  38614  eqvrelcoss2  38616  dfcoeleqvrel  38619  refrelredund4  38632  cnvepresdmqs  38651  dfcomember  38670  dfdisjALTV  38711  dfeldisj3  38717  dfeldisj4  38718  dfeldisj5  38719  disjres  38742  prter1  38878  islshp  38978  islshpat  39016  lcvbr2  39021  lcvnbtwn2  39026  cvrnbtwn3  39275  isatl  39298  ishlat1  39351  ishlat2  39352  cvrat4  39442  pmapglbx  39768  lhpexle3  40011  dib1dim  41164  diblsmopel  41170  lcfls1lem  41533  prjsperref  42599  prjspeclsp  42605  euabsn2w  42672  rexrabdioph  42787  dford4  43022  onsupuni  43222  dflim6  43257  tfsconcatlem  43329  naddgeoa  43387  ifpdfor2  43454  ifpdfan2  43456  ifpdfor  43458  ifpdfan  43459  ifpnot23b  43475  ifpnot23c  43477  ifpnot23d  43478  ifpim123g  43493  ifpbibib  43503  clss2lem  43604  imaiun1  43644  coiun1  43645  brfvrcld2  43685  iunrelexp0  43695  brtrclfv2  43720  snhesn  43779  dffrege76  43932  frege97  43953  frege98  43954  frege109  43965  frege110  43966  dffrege115  43971  frege131  43987  frege133  43989  ntrneineine1lem  44077  ntrneiel2  44079  ntrneiiso  44084  gneispace3  44126  scotteld  44239  ismnuprim  44287  ismnushort  44294  dfuniv2  44295  pm11.52  44380  pm11.58  44383  pm13.192  44403  impexpdcom  44509  sbc3or  44526  opelopab4  44545  uunT12p1  44793  uunT12p2  44794  uunT12p3  44795  uun2221  44806  uun2221p1  44807  uun2221p2  44808  undif3VD  44875  modelaxreplem3  44974  permaxext  44999  permac8prim  45008  ndisj2  45049  nssrex  45084  rabssf  45117  bothtbothsame  46903  bothfbothsame  46904  aiffbtbat  46912  reuabaiotaiota  47091  2reu8i  47117  2reuimp0  47118  ichn  47460  dfodd2  47640  dfeven5  47670  dfodd7  47671  1nevenALTV  47695  oddprmne2  47719  dfvopnbgr2  47857  isuspgrim0lem  47897  gpg5nbgrvtx03starlem1  48072  gpg5nbgrvtx03starlem2  48073  gpg5nbgrvtx03starlem3  48074  gpg5nbgrvtx13starlem1  48075  gpg5nbgrvtx13starlem2  48076  gpg5nbgrvtx13starlem3  48077  gpg5edgnedg  48134  islindeps2  48488  isldepslvec2  48490  line2xlem  48758  rmotru  48807  reutru  48808  isnrm4  48935  iscnrm4  48958  homf0  49014  fuco2el  49317  isthincd2  49442  thinccic  49476  istermc2  49480  istermc3  49481  dftermc3  49536  setrec1lem3  49694  aacllem  49806