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

Syntax hints:   ↔ wb 205

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 206

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  641  mpbiran  708  biadaniALT  820  imor  852  imimorb  949  pm5.6  1000  nbi2  1014  casesifp  1076  3ancoma  1096  3ancomb  1097  3anrev  1099  dfnan2  1488  nannan  1491  nanbi  1494  xorcom  1508  xorneg  1517  xorbi12i  1518  norcom  1524  noran  1526  norasslem1  1528  trunortru  1583  trunorfal  1584  cadan  1603  cadcomb  1607  nic-ax  1668  nic-axALT  1669  nf3  1781  nfnbiOLD  1851  19.43  1878  equsv  1999  sbrimvw  2087  sbcom2  2163  sb5  2263  nf5  2272  nf6  2273  sbrim  2294  sbnf  2302  sb6x  2459  2sb5rf  2467  2sb6rf  2468  sb4b  2470  sb5f  2493  sbequ8  2496  sbhb  2516  eu6lem  2563  eu1  2602  issetlem  2809  cleqh  2859  clelabOLD  2876  cleqf  2930  sbabel  2934  necon3bii  2989  neor  3030  neorian  3033  rextru  3073  r19.26m  3106  r19.43  3118  r2allem  3138  r19.23t  3248  ralcom4  3279  rexcomOLD  3284  moel  3394  moelOLD  3397  rabid2f  3459  rabid2OLD  3461  eqv  3479  eqvf  3480  ralv  3495  rexv  3496  reuv  3497  rmov  3498  rexcom4b  3500  ceqsex4v  3529  ceqsex8v  3531  ceqsrexv  3640  rexab  3688  ralrab2  3692  rexrab2  3694  reu2  3719  reu3  3721  reueq  3731  2reuswap  3740  2reuswap2  3741  reuind  3747  2reu5lem3  3751  2rmoswap  3755  rmo2  3878  rmoanim  3885  rmoanimALT  3886  dfss2  3965  dfss2OLD  3966  dfss3  3967  dfss3f  3970  ssabral  4056  rabss  4066  ssrabeq  4079  uniiunlem  4081  sspsstri  4099  npss  4107  dfdif3  4111  raldifb  4141  uncom  4150  inass  4216  elsymdifxor  4246  nsspssun  4254  dfss4  4255  dfun2  4256  dfin2  4257  indi  4270  indifdirOLD  4282  reupick3  4316  eq0f  4337  neq0f  4338  eq0  4340  eq0ALT  4341  dfnf5  4374  rabn0  4382  csbab  4434  vss  4440  disj  4444  disjOLD  4445  disj3  4450  undisj1  4458  undisj2  4459  inundif  4475  undif  4478  undifr  4479  rabsssn  4667  exsnrex  4681  euabsn2  4726  euabsn  4727  raldifsni  4795  tppreqb  4805  pwpw0  4813  prssg  4819  ssunsn  4828  preqsn  4859  pwpr  4898  dfuni2  4906  unissb  4938  unissbOLD  4939  elint2  4952  ssint  4963  uniintab  4987  dfiin2g  5030  iunid  5058  iunn0  5065  iunxun  5092  iunxiun  5095  iinpw  5104  disjor  5123  disjxiun  5140  dftr2  5262  dftr5OLD  5265  dftr3  5266  dftr4  5267  axrep6  5287  vnex  5309  inuni  5340  eusv2  5391  reusv2lem4  5396  rexxfr  5411  sspwb  5446  opthneg  5478  pwssun  5568  dfid3  5574  dffr6  5631  dffr2  5637  dffr2ALT  5638  opthprc  5737  elxp3  5739  xpiundir  5744  elvv  5747  reliun  5813  inxpOLD  5830  raliunxp  5837  cnvuni  5884  dmopab2rex  5915  dm0rn0  5922  dfres3  5985  ssdmres  6003  elidinxp  6042  idinxpres  6045  dfima2  6060  args  6091  dffr3  6098  cotrg  6108  cotrgOLD  6109  cotrgOLDOLD  6110  intasym  6116  asymref  6117  intirr  6119  xpnz  6158  xp11  6174  ssrnres  6177  xpimasn  6184  coiun  6255  coass  6264  cnvso  6287  elsnxp  6290  dfpo2  6295  imaindm  6298  dffr4  6320  dfse3  6337  frpoind  6343  wfiOLD  6352  dflim2  6421  orddif  6460  dffun2OLDOLD  6555  dffun6  6556  dffun6f  6561  dffun7  6575  dffun9  6577  funfn  6578  svrelfun  6620  mptfnf  6685  dffn2  6719  dffn3  6730  fint  6771  dffn4  6812  dff1o4  6842  brprcneu  6882  brprcneuALT  6883  eqfnfv3  7037  fnreseql  7052  fsn  7139  ftpg  7160  abrexco  7249  imaiun  7250  dff13  7260  isof1oidb  7327  isof1oopb  7328  isocnv2  7334  eloprabga  7523  mpo2eqb  7548  elovmpo  7661  sorpss  7728  abexex  7970  elxp6  8022  elxp7  8023  releldm2  8042  opiota  8058  fnmpo  8068  frxp  8126  frxp2  8144  soseq  8159  cnvimadfsn  8171  mpoxneldm  8212  dftpos4  8245  frrlem9  8294  wfrlem8OLD  8331  wfrfunOLD  8334  dfrecs3  8387  dfrecs3OLD  8388  tfrlem7  8398  ondif1  8516  oarec  8577  oeeu  8618  0er  8756  eroveu  8825  erovlem  8826  elixpconst  8918  domen  8976  brsdom  8990  brdom2  8997  reuen1  9044  sbthlem10  9111  brsdom2  9116  xpf1o  9158  unfi  9191  sbthfilem  9220  onfin2  9250  0sdom1domALT  9258  modom  9263  unfiOLD  9332  marypha2lem3  9455  wemapsolem  9568  elom3  9666  dfom5  9668  brttrcl2  9732  ttrcltr  9734  ttrclse  9745  trcl  9746  epfrs  9749  frind  9768  rankf  9812  scottexs  9905  scott0s  9906  cplem1  9907  hta  9915  djuexb  9927  pm54.43lem  10018  alephsuc2  10098  iscard3  10111  aceq0  10136  aceq3lem  10138  dfac3  10139  dfac5lem2  10142  dfac5  10146  dfac7  10150  dfac12a  10166  kmlem12  10179  kmlem14  10181  kmlem15  10182  infmap2  10236  ackbij2  10261  dfacfin7  10417  ituniiun  10440  zorng  10522  brdom7disj  10549  entri2  10576  alephreg  10600  fpwwe2lem11  10659  fpwwe2lem12  10660  pwfseqlem1  10676  grutsk  10840  axgroth4  10850  grothprim  10852  grothtsk  10853  elni2  10895  ltsopi  10906  genpass  11027  psslinpr  11049  ltexprlem4  11057  ltresr  11158  1re  11239  infm3  12198  elnnz  12593  dfz2  12602  2rexuz  12909  nnwos  12924  eluz2b1  12928  qexALT  12973  elxr  13123  dflt2  13154  xrsupss  13315  xrinfmss  13316  elixx1  13360  elioo2  13392  dfrp2  13400  elioopnf  13447  elicopnf  13449  elfz1  13516  fznn  13596  fzp1nel  13612  fznn0  13620  preduz  13650  prinfzo0  13698  injresinj  13780  nn0opthlem1  14254  faclbnd4lem1  14279  hashfxnn0  14323  hashprdifel  14384  hashgt23el  14410  hashfun  14423  hashf1  14445  fz1isolem  14449  f1oun2prg  14895  brtrclfv  14976  shftdm  15045  rediv  15105  imdiv  15112  rexanre  15320  caubnd  15332  climreu  15527  prodmo  15907  dvdslelem  16280  3dvdsdec  16303  3dvds2dec  16304  bitsval  16393  smueqlem  16459  algcvgblem  16542  lcmfunsnlem2  16605  isprm2  16647  isprm3  16648  isprm4  16649  pythagtriplem2  16780  elgz  16894  hashbc0  16968  0ram  16983  isstruct  17115  issect  17730  isfull2  17894  isfth2  17898  fucinv  17959  eldmcoa  18048  isdrs  18287  submacs  18773  isnsg4  19116  isgim  19210  gaorb  19252  oppgid  19304  oppgsubm  19310  oppgcntz  19312  ispgp  19541  efgsdm  19679  efgcpbllema  19703  iscyg2  19831  isrng  20088  isring  20171  isirred2  20354  opprirred  20355  isrnghm  20374  dfrhm2  20407  isnzr2  20451  opprsubrng  20490  opprsubrg  20526  drngid2  20639  issdrg  20670  islmod  20741  lss1d  20841  islmhm  20906  islmim  20941  lbsextlem2  21041  lidlnz  21131  isdomn3  21242  dfprm2  21393  isphl  21554  elocv  21594  iunocv  21607  isobs  21648  islinds  21737  1mavmul  22444  toprntopon  22821  isbasis3g  22846  fctop  22901  cctop  22903  isclo2  22986  restsn  23068  lmbr  23156  ist0-3  23243  2ndcdisj  23354  1stccnp  23360  islocfin  23415  1stckgenlem  23451  txbas  23465  ptbasin  23475  tx2cn  23508  fbfinnfr  23739  fbasrn  23782  filuni  23783  ufinffr  23827  fin1aufil  23830  rnelfmlem  23850  flimrest  23881  alexsubALTlem3  23947  alexsubALTlem4  23948  tgphaus  24015  istlm  24083  iscusp2  24201  metuel2  24468  isngp2  24500  isnlm  24586  isphtpc  24914  phtpcer  24915  om1elbas  24953  isclm  24985  iscvsp  25049  iscph  25092  iscau3  25200  minveclem3b  25350  elovolm  25398  ioombl1lem4  25484  dyaddisj  25519  vitali  25536  itg1climres  25638  itg2seq  25666  itg2monolem1  25674  itg2mono  25677  limcrcl  25797  lhop1  25941  itgsubst  25978  mdegleb  25994  isuc1p  26070  ismon1p  26072  plydivex  26226  ellogdm  26567  1cubr  26768  atandm2  26803  birthdaylem3  26879  dmarea  26883  dchrelbas2  27164  dchrelbas4  27170  elno3  27582  nosgnn0  27585  nosepon  27592  nocvxminlem  27704  scutcut  27728  scutbday  27731  dmscut  27738  scutf  27739  sltrec  27747  made0  27794  addsprop  27887  negsproplem2  27935  negsprop  27941  mulsprop  28024  precsexlem10  28108  recut  28218  0reno  28219  axcontlem7  28775  nb3grpr  29189  nb3grpr2  29190  upgrwlkcompim  29451  wlkson  29464  wlkonprop  29466  wksonproplem  29512  wksonproplemOLD  29513  ispth  29531  wwlknon  29662  wwlksnextinj  29704  wspthsnwspthsnon  29721  elwspths2spth  29772  rusgrnumwwlkl1  29773  clwwlkccatlem  29793  erclwwlkref  29824  frgr3v  30079  nmoubi  30576  nmobndseqi  30583  nmobndseqiALT  30584  minvecolem1  30678  isch2  31027  hlimreui  31043  isch3  31045  ocsh  31087  dfch2  31211  spanuni  31348  nonbooli  31455  5oalem7  31464  adjsym  31637  elbdop2  31675  dmadjss  31691  nmopub  31712  nmfnleub  31729  nmop0h  31795  pjssposi  31976  pjordi  31977  cvbr2  32087  cvnbtwn2  32091  mdsl2i  32126  cvmdi  32128  elat2  32144  atom1d  32157  chirredi  32198  cdj3i  32245  or3di  32253  opreu2reu1  32276  mo5f  32281  reuxfrdf  32283  rexunirn  32284  difrab2  32290  iuninc  32345  disjorf  32363  disjunsn  32378  rabfmpunirn  32433  aciunf1  32443  funcnv5mpt  32448  eliccelico  32540  elicoelioo  32541  isomnd  32776  omndmul2  32787  isslmd  32904  islinds5  33074  ismxidl  33170  hasheuni  33699  pwsiga  33744  sigainb  33750  issros  33789  2ndmbfm  33876  omssubaddlem  33914  omssubadd  33915  sitgaddlemb  33963  eulerpartlemgvv  33991  eulerpartlemn  33996  probun  34034  ballotlem2  34103  ballotlemodife  34112  bnj252  34329  bnj253  34330  bnj255  34331  bnj345  34340  bnj133  34353  bnj976  34403  bnj1098  34409  bnj121  34496  bnj130  34500  bnj150  34502  bnj581  34534  bnj607  34542  bnj865  34549  bnj917  34560  bnj934  34561  bnj964  34569  bnj983  34577  bnj996  34582  bnj1021  34592  bnj1033  34595  bnj1047  34599  bnj1049  34600  bnj1090  34605  bnj1128  34616  bnj1175  34630  bnj1189  34635  bnj1253  34643  bnj1312  34684  exdifsn  34699  fineqvrep  34710  fineqvac  34712  erdszelem9  34804  erdszelem10  34805  pconnconn  34836  cvmliftiota  34906  fmlaomn0  34995  fmla0disjsuc  35003  fmlasucdisj  35004  dmopab3rexdif  35010  elmthm  35181  nepss  35307  xpab  35315  dfso2  35344  elrn3  35351  elpotr  35372  dfon2lem5  35378  dfon2lem7  35380  dfon2lem8  35381  elwlim  35414  wzel  35415  brtxp2  35472  brpprod3a  35477  eltrans  35482  dfon3  35483  dffix2  35496  dffun10  35505  elfuns  35506  brsingle  35508  brimg  35528  funpartfun  35534  funpartfv  35536  cgrxfr  35646  segletr  35705  outsideoftr  35720  neifg  35850  filnetlem4  35860  df3nandALT1  35878  bj-consensusALT  36050  bj-df-ifc  36051  bj-biexal3  36179  bj-nfnnfTEMP  36230  bj-denoteslem  36343  bj-denotes  36344  bj-ralvw  36352  bj-rexvw  36353  bj-rexcom4bv  36355  bj-rexcom4b  36356  bj-sbeq  36374  bj-inrab  36400  bj-rcleqf  36499  bj-dfmpoa  36592  bj-imdirco  36664  topdifinffinlem  36821  topdifinfeq  36824  relowlssretop  36837  relowlpssretop  36838  rdgeqoa  36844  domalom  36878  nlpineqsn  36882  fvineqsneq  36886  wl-ifpimpr  36940  wl-df3xor3  36944  wl-3xorbi  36947  wl-3xorbi2  36948  wl-2xor  36957  wl-2mintru2  36965  wl-dfclab  37058  rabiun  37061  phpreu  37072  fin2solem  37074  matunitlindflem2  37085  ptrest  37087  poimirlem25  37113  poimirlem27  37115  poimirlem30  37118  ismblfin  37129  ovoliunnfl  37130  voliunnfl  37132  volsupnfl  37133  itg2addnclem2  37140  fdc  37213  prdstotbnd  37262  isdrngo1  37424  ispridl  37502  ismaxidl  37508  impor  37549  selconj  37568  tradd  37573  scott0f  37637  r2alan  37715  inxpss3  37781  idinxpssinxp2  37785  idinxpssinxp3  37786  dfrel5  37813  ineleq  37821  moantr  37831  dfxrn2  37843  inxpxrn  37862  rnxrnres  37866  coss1cnvres  37884  1cossres  37896  cocossss  37903  cossssid4  37937  cossssid5  37938  cosscnvssid5  37945  cossid  37947  dfssr2  37966  cnvrefrelcoss2  38004  cosselcnvrefrels2  38005  eqvrelcoss  38084  eqvrelcoss2  38086  dfcoeleqvrel  38089  refrelredund4  38102  cnvepresdmqs  38120  dfcomember  38139  dfdisjALTV  38180  dfeldisj3  38186  dfeldisj4  38187  dfeldisj5  38188  disjres  38211  prter1  38346  islshp  38446  islshpat  38484  lcvbr2  38489  lcvnbtwn2  38494  cvrnbtwn3  38743  isatl  38766  ishlat1  38819  ishlat2  38820  cvrat4  38911  pmapglbx  39237  lhpexle3  39480  dib1dim  40633  diblsmopel  40639  lcfls1lem  41002  prjsperref  42021  prjspeclsp  42027  rexrabdioph  42205  dford4  42441  onsupuni  42648  dflim6  42684  tfsconcatlem  42756  naddgeoa  42815  ifpdfor2  42882  ifpdfan2  42884  ifpdfor  42886  ifpdfan  42887  ifpnot23b  42903  ifpnot23c  42905  ifpnot23d  42906  ifpim123g  42921  ifpbibib  42931  clss2lem  43032  imaiun1  43072  coiun1  43073  brfvrcld2  43113  iunrelexp0  43123  brtrclfv2  43148  snhesn  43207  dffrege76  43360  frege97  43381  frege98  43382  frege109  43393  frege110  43394  dffrege115  43399  frege131  43415  frege133  43417  ntrneineine1lem  43505  ntrneiel2  43507  ntrneiiso  43512  gneispace3  43554  scotteld  43674  ismnuprim  43722  ismnushort  43729  dfuniv2  43730  pm11.52  43815  pm11.58  43818  pm13.192  43838  impexpdcom  43945  sbc3or  43962  opelopab4  43981  uunT12p1  44230  uunT12p2  44231  uunT12p3  44232  uun2221  44243  uun2221p1  44244  uun2221p2  44245  undif3VD  44312  ndisj2  44406  nssrex  44443  rabssf  44476  bothtbothsame  46272  bothfbothsame  46273  aiffbtbat  46281  reuabaiotaiota  46458  2reu8i  46484  2reuimp0  46485  ichn  46787  dfodd2  46967  dfeven5  46997  dfodd7  46998  1nevenALTV  47022  oddprmne2  47046  isuspgrim0lem  47160  gricer  47181  islindeps2  47542  isldepslvec2  47544  line2xlem  47817  rmotru  47866  reutru  47867  isnrm4  47940  iscnrm4  47964  isthincd2  48035  thinccic  48058  setrec1lem3  48111  aacllem  48225

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »