MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr4i Structured version   Visualization version   GIF version

Theorem 3bitr4i 292
Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
3bitr4i.1 (𝜑𝜓)
3bitr4i.2 (𝜒𝜑)
3bitr4i.3 (𝜃𝜓)
Assertion
Ref Expression
3bitr4i (𝜒𝜃)

Proof of Theorem 3bitr4i
StepHypRef Expression
1 3bitr4i.2 . 2 (𝜒𝜑)
2 3bitr4i.1 . . 3 (𝜑𝜓)
3 3bitr4i.3 . . 3 (𝜃𝜓)
42, 3bitr4i 267 . 2 (𝜑𝜃)
51, 4bitri 264 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  bibi2d  331  or4  549  pm4.14  601  pm4.71  663  pm5.32ri  671  an31  858  an4  882  orimdi  910  ordi  926  ordir  927  andir  930  orbidi  993  dfbi3  1018  dfbi3OLD  1019  dfifp7  1039  ifpn  1042  3anrot  1060  3orrot  1061  3ancoma  1062  3orcoma  1063  3orcombOLD  1066  3ioran  1073  3ianor  1074  3anbi123i  1270  3orbi123i  1271  an6  1448  3or6  1450  an33rean  1486  xorcom  1507  xorass  1508  xorbi12i  1517  anxordi  1519  hadbi  1577  hadcoma  1578  hadcomb  1579  hadnot  1581  cador  1587  cadan  1588  cadcoma  1591  cadnot  1594  nic-axALT  1639  nfnbi  1821  19.26-3an  1840  19.43OLD  1851  nfbiiOLD  1876  19.32v  1909  19.31v  1910  19.42v  1921  4exdistr  1927  sbequ8  1942  equsalvw  1977  cbvexvw  2012  excom  2082  19.32  2139  19.31  2140  19.42  2143  equsalv  2146  equsalhw  2161  cbvexv1  2212  eeeanv  2219  cbvex  2308  cbvexv  2311  cbvex2  2316  equsal  2327  dfsb3  2402  sbor  2426  sban  2427  sbbi  2429  sbnf2  2467  sbcom4  2474  sbex  2491  eu5  2524  sb8eu  2532  sb8mo  2533  cbvmo  2535  eu1  2539  sbmo  2544  abeq1  2762  cbvab  2775  sbabel  2822  r2allem  2966  r19.21v  2989  ralbii2  3007  rexbii2  3068  r19.30  3111  r19.32v  3112  r19.41v  3118  r19.41  3119  r19.42v  3121  r19.43  3122  ralcomf  3125  rexcomf  3126  reean  3135  3reeanv  3137  2ralor  3138  rabid2  3148  rabid2f  3149  rabbi  3150  reubiia  3157  rmobiia  3162  reu5  3189  rmo5  3192  cbvralf  3195  cbvrexf  3196  cbvreu  3199  cbvrmo  3200  vjust  3232  abv  3237  ceqsex3v  3277  ceqsex4v  3278  ceqsex8v  3280  eueq  3411  reu2  3427  reu6  3428  reu3  3429  rmo4  3432  2reu5  3449  cbvsbc  3497  sbccomlem  3541  rmo3  3561  cbvralcsf  3598  cbvrexcsf  3599  cbvreucsf  3600  eqss  3651  uniiunlem  3724  sspsstri  3742  compleq  3785  ssequn1  3816  unss  3820  rexun  3826  ralunb  3827  elin3  3837  incom  3838  inass  3856  ssin  3868  elsymdif  3882  elsymdifxor  3883  symdif2  3885  symdifass  3886  nssinpss  3889  dfun2  3892  difin  3894  indi  3906  indifdir  3916  ssdif0  3975  inssdif0  3980  dfnf5  3985  rabeq0  3990  rabn0OLD  3992  disj3  4054  ssundif  4085  dfif2  4121  eldifpr  4237  rexsns  4249  snprc  4285  reusn  4294  difsnpss  4370  prssOLD  4384  tpss  4400  preqsn  4424  pwpr  4462  eluni2  4472  elunirab  4480  uniun  4488  unissb  4501  elintrab  4520  ssintrab  4532  intun  4541  intpr  4542  iuncom  4559  iuncom4  4560  iunab  4598  ssiinf  4601  iunn0  4612  iinab  4613  iunin2  4616  iinun2  4618  iundif2  4619  iunun  4636  iunxun  4637  iunxiun  4640  sspwuni  4643  iinpw  4649  cbvdisj  4662  disjor  4666  brun  4736  brin  4737  brdif  4738  dftr2  4787  intexrab  4853  inuni  4856  ssext  4953  pweqb  4955  otth2  4981  snopeqop  4998  propeqop  4999  opelopabsbALT  5013  eqopab2b  5034  pwin  5047  pwun  5051  elxp2  5166  xpiundi  5207  xpiundir  5208  poinxp  5216  soinxp  5217  frinxp  5218  seinxp  5219  weinxp  5220  inopab  5285  difopab  5286  raliunxp  5294  rexiunxp  5295  rexxpf  5302  iunxpf  5303  cnvco  5340  dmiun  5365  dmuni  5366  dm0rn0  5374  brresOLD  5439  dmres  5454  restidsing  5493  restidsingOLD  5494  cnvsym  5545  asymref  5547  codir  5551  qfto  5552  cnvopab  5568  cnvdif  5574  rniun  5578  dminss  5582  imainss  5583  difxp  5593  xpdifid  5597  dmsnn0  5635  cnvcnvsn  5648  cnvresima  5661  resco  5677  imaco  5678  rnco  5679  coiun  5683  coass  5692  ressn  5709  cnviin  5710  cnvpo  5711  cnvso  5712  xpco  5713  dflim2  5819  unisuc  5839  funcnv  5996  funcnv3  5997  fncnv  6000  fun11  6001  imadif  6011  fnres  6045  dfmpt3  6052  mptfnf  6053  fnopabg  6055  fint  6122  fin  6123  fores  6162  dff1o3  6181  f1ompt  6422  fsn  6442  imaiun  6543  isocnv2  6621  isocnv3  6622  isores2  6623  isomin  6627  eqoprab2b  6755  sucexb  7051  sucelon  7059  dflim4  7090  fun11iun  7168  f11o  7170  opabex3d  7187  opabex3  7188  dfopab2  7266  dfoprab3s  7267  fmpt2x  7281  fparlem1  7322  fparlem2  7323  fsplit  7327  suppvalbr  7344  tpostpos  7417  wfrlem8  7467  wfrfun  7470  dfsmo2  7489  brwitnlem  7632  oarec  7687  qsid  7856  uniinqs  7870  mapval2  7929  mapsncnv  7946  elixp2  7954  ixpin  7975  brsdom  8020  brdom2  8027  xpassen  8095  brsdom2  8125  unfilem1  8265  fiint  8278  dfsup2  8391  supmo  8399  eqinf  8431  infmo  8442  rankc1  8771  cp  8792  isinfcard  8953  aceq1  8978  aceq2  8980  dfac5lem3  8986  dfac10b  8999  dfac12a  9008  dffin7-2  9258  dfacfin7  9259  fin1a2lem6  9265  iunfo  9399  konigthlem  9428  axgroth6  9688  axgroth3  9691  sstskm  9702  ltexprlem1  9896  gt0srpr  9937  ltpsrpr  9968  map2psrpr  9969  ltresr  9999  fimaxre3  11008  sup3  11018  supaddc  11028  supmul1  11030  elnn0z  11428  elznn0nn  11429  zmin  11822  xrnemnf  11989  xrnepnf  11990  elioomnf  12306  elxrge0  12319  elfzuzb  12374  fzass4  12417  elfz2nn0  12469  elfzo2  12512  elfzo3  12525  lbfzo0  12547  fzind2  12626  nn0opthlem1  13095  cotr2g  13761  rexfiuz  14131  fsumcom2  14549  fsumcom2OLD  14550  prodmo  14710  fprodcom2  14758  fprodcom2OLD  14759  sinltx  14963  divalglem4  15166  divalglem10  15172  4sqlem12  15707  imasleval  16248  xpsfrnel  16270  xpscf  16273  isssc  16527  isffth2  16623  ispos2  16995  ismhm  17384  nsgacs  17677  isgim  17751  oppgcntz  17840  f1omvdco3  17915  pmtrprfvalrn  17954  efgrelexlemb  18209  pgpfac1  18525  pgpfac  18529  issrg  18553  opprsubg  18682  opprunit  18707  isirred2  18747  opprirred  18748  drngprop  18806  opprdrng  18819  islss  18983  islbs  19124  isdomn2  19347  unocv  20072  iunocv  20073  fvmptnn04if  20702  isbasis2g  20800  tgval2  20808  ntreq0  20929  isclo2  20940  cmpcov2  21241  is1stc2  21293  1stcelcls  21312  llyi  21325  unisngl  21378  txuni2  21416  xkobval  21437  hausdiag  21496  isfbas2  21686  elfg  21722  fbasrn  21735  fmfnfmlem3  21807  isfcls  21860  alexsubALTlem2  21899  istmd  21925  istgp  21928  istrg  22014  istdrg  22016  istdrg2  22028  isms2  22302  metuel2  22417  restmetu  22422  isngp  22447  isngp2  22448  isngp3  22449  elii1  22781  isncvsngp  22995  iscph  23016  isbn  23181  pmltpc  23265  ovolfcl  23281  finiunmbl  23358  iundisj  23362  dyaddisj  23410  vitalilem1  23422  ellimc3  23688  ig1pval3  23979  plyun0  23998  plydivex  24097  aannenlem2  24129  ellogrn  24351  atandm  24648  atandm3  24650  atans2  24703  colinearalg  25835  axeuclid  25888  nbgrsym  26308  upgrtrls  26654  upgristrl  26655  usgr2pth0  26717  iswwlks  26784  isclwwlk  26952  clwwlkneq0  26990  h2hlm  27965  issh  28193  chcon2i  28451  chcon1i  28452  chcon3i  28453  chnlei  28472  cmcm2i  28580  cmcm3i  28581  3oalem3  28651  pjdifnormii  28670  pjneli  28710  dfadj2  28872  cnvadj  28879  hhcno  28891  hhcnf  28892  eleigvec  28944  eleigvec2  28945  pjimai  29163  isst  29200  ishst  29201  cvnbtwn4  29276  chrelat4i  29360  moel  29451  rmo3f  29462  rmo4fOLD  29463  difrab2  29465  iunin1f  29500  disjnf  29510  cbvdisjf  29511  disjorf  29518  iundisjf  29528  disjexc  29532  dfrp2  29660  xrdifh  29670  iundisjfi  29683  xrnarchi  29866  isorng  29927  pmtrprfv2  29976  cmpcref  30045  ordtconnlem1  30098  isrrext  30172  cntnevol  30419  ddemeas  30427  omssubaddlem  30489  omssubadd  30490  eulerpartleme  30553  eulerpartlemv  30554  eulerpartlemt0  30559  eulerpartlemgvv  30566  eulerpartlemn  30571  ballotlem2  30678  ballotlemodife  30687  oddprm2  30861  bnj257  30901  bnj268  30903  bnj290  30904  bnj312  30906  bnj89  30915  bnj538OLD  30936  bnj887  30961  bnj976  30974  bnj1019  30976  bnj1146  30988  bnj1385  31029  bnj110  31054  bnj121  31066  bnj130  31070  bnj153  31076  bnj543  31089  bnj580  31109  bnj607  31112  bnj849  31121  bnj882  31122  bnj916  31129  bnj985  31149  bnj1033  31163  bnj1083  31172  bnj1090  31173  bnj1128  31184  bnj1174  31197  bnj1228  31205  erdszelem1  31299  cvmliftlem15  31406  snmlval  31439  elmpst  31559  mpstrcl  31564  untuni  31712  dfso3  31727  dftr6  31766  coep  31767  coepr  31768  dffr5  31769  dfso2  31770  dfpo2  31771  cnvco1  31775  cnvco2  31776  eldm3  31777  dfdm5  31800  dfrn5  31801  imaindm  31806  frrlem5c  31911  elno3  31933  conway  32035  madeval2  32061  brsset  32121  idsset  32122  dfon3  32124  dfbigcup2  32131  dfom5b  32144  dffun10  32146  dfiota3  32155  fnimage  32161  brdomain  32165  brrange  32166  brimg  32169  brapply  32170  brcup  32171  brcap  32172  brsuccf  32173  funpartlem  32174  brrestrict  32181  dfrecs2  32182  brub  32186  altopelaltxp  32208  trer  32435  filnetlem4  32501  df3nandALT1  32521  imnand2  32524  bj-dfbi5  32684  bj-ssbssblem  32774  bj-ssbcom3lem  32775  bj-cbvex2v  32863  bj-abeq1  32899  bj-vjust  32911  bj-sbnf  32953  bj-ralcom4  32993  bj-csbsnlem  33023  bj-sscon  33139  bj-restpw  33170  wl-nancom  33427  iundif1  33513  poimirlem25  33564  poimirlem26  33565  poimirlem30  33569  ismblfin  33580  mbfposadd  33587  itg2addnclem2  33592  ftc1anc  33623  inixp  33653  prdstotbnd  33723  heibor1lem  33738  isrngohom  33894  isidl  33943  isfldidl2  33998  isdmn3  34003  sbccom2lem  34059  triantru3  34143  vvdifopab  34165  brres2  34176  eldmqsres  34192  inxpss  34223  n0el2  34244  trcoss2  34374  pmapglbx  35373  lhpexle3  35616  cdleme25cv  35963  dicelval3  36786  diclspsn  36800  lcfls1c  37142  moxfr  37572  fphpd  37697  issdrg2  38085  ifpim1  38130  ifpnot  38131  ifpid2  38132  ifpim2  38133  ifpxorcor  38138  ifpnot23  38140  ifpananb  38168  ifpnannanb  38169  ifpxorxorb  38173  rp-fakeinunass  38178  undmrnresiss  38227  cnvssco  38229  cotrintab  38238  cnviun  38259  imaiun1  38260  coiun1  38261  elintima  38262  frege133d  38374  frege54cor0a  38474  or3or  38636  andi3or  38637  ntrneikb  38709  ntrneixb  38710  ntrneik4w  38715  k0004lem1  38762  undisjrab  38822  nzss  38833  pm10.541  38883  compab  38962  conss34OLD  38963  onfrALTlem5  39074  csbabgOLD  39367  onfrALTlem5VD  39435  inn0f  39556  eluni2f  39600  r19.32  41488  rmoanim  41500  3an4ancom24  41610  issubmgm  42114  sgrp2sgrp  42189  islindeps  42567  elbigo  42670  setrec1lem3  42761  elpg  42785
  Copyright terms: Public domain W3C validator