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

Theorem 3bitr4i 291
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 266 . 2 (𝜑𝜃)
51, 4bitri 263 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  bibi2d  331  or4  549  pm4.14  600  pm4.71  660  pm5.32ri  668  an31  837  an4  861  orimdi  888  ordi  904  ordir  905  andir  908  dfbi3  933  orbidi  969  dfifp7  1013  ifpn  1016  3anrot  1036  3orrot  1037  3ancoma  1038  3orcoma  1039  3orcomb  1041  3ioran  1049  3anbi123i  1244  3orbi123i  1245  an6  1400  3or6  1402  an33rean  1438  xorcom  1459  xorass  1460  xorbi12i  1469  anxordi  1471  hadbi  1528  hadcoma  1529  hadcomb  1530  hadnot  1532  cador  1538  cadan  1539  cadcoma  1542  cadnot  1545  nic-axALT  1590  nfbii  1770  19.26-3an  1788  19.43OLD  1800  nfbiiOLD  1824  19.32v  1856  19.31v  1857  sbequ8  1872  19.42v  1905  4exdistr  1911  equsalvw  1918  cbvexvw  1957  excom  2029  19.32  2088  19.31  2089  19.42  2092  equsalhw  2109  cbvexv1  2164  eeeanv  2171  cbvex  2260  cbvexv  2263  cbvex2  2268  equsal  2279  dfsb3  2362  sbor  2386  sban  2387  sbbi  2389  sbnf2  2427  sbcom4  2434  sbex  2451  eu5  2484  sb8eu  2491  sb8mo  2492  cbvmo  2494  eu1  2498  sbmo  2503  abeq1  2720  cbvab  2733  sbabel  2779  r2allem  2921  r19.21v  2943  ralbii2  2961  rexbii2  3021  r19.30  3063  r19.32v  3064  r19.41v  3070  r19.41  3071  r19.42v  3073  r19.43  3074  ralcomf  3077  rexcomf  3078  reean  3085  3reeanv  3087  2ralor  3088  rabid2  3096  rabbi  3097  reubiia  3104  rmobiia  3109  reu5  3136  rmo5  3139  cbvralf  3141  cbvrexf  3142  cbvreu  3145  cbvrmo  3146  vjust  3174  abv  3179  ceqsex3v  3219  ceqsex4v  3220  ceqsex8v  3222  eueq  3345  reu2  3361  reu6  3362  reu3  3363  rmo4  3366  2reu5  3383  cbvsbc  3431  sbccomlem  3475  rmo3  3494  cbvralcsf  3531  cbvrexcsf  3532  cbvreucsf  3533  eqss  3583  uniiunlem  3653  sspsstri  3671  compleq  3714  ssequn1  3745  unss  3749  rexun  3755  ralunb  3756  elin3  3766  incom  3767  inass  3785  ssin  3797  elsymdif  3811  elsymdifxor  3812  symdif2  3814  symdifass  3815  nssinpss  3818  dfun2  3821  difin  3823  indi  3832  indifdir  3842  ssdif0  3896  inssdif0  3901  dfnf5  3906  rabeq0  3911  rabn0OLD  3913  disj3  3973  ssundif  4004  dfif2  4038  eldifpr  4152  rexsns  4164  snprc  4197  reusn  4206  difsnpss  4279  prssOLD  4292  tpss  4308  preqsn  4331  pwpr  4368  eluni2  4376  elunirab  4384  uniun  4392  unissb  4405  elintrab  4423  ssintrab  4435  intun  4444  intpr  4445  iuncom  4463  iuncom4  4464  iunab  4502  ssiinf  4505  iunn0  4516  iinab  4517  iunin2  4520  iinun2  4522  iundif2  4523  iunun  4540  iunxun  4541  iunxiun  4544  sspwuni  4547  iinpw  4550  cbvdisj  4563  disjor  4567  brun  4633  brin  4634  brdif  4635  dftr2  4682  intexrab  4750  inuni  4753  ssext  4850  pweqb  4852  otth2  4878  snopeqop  4894  propeqop  4895  opelopabsbALT  4909  eqopab2b  4930  pwin  4942  pwun  4946  elxp2  5056  xpiundi  5096  xpiundir  5097  poinxp  5105  soinxp  5106  frinxp  5107  seinxp  5108  weinxp  5109  inopab  5174  difopab  5175  raliunxp  5183  rexiunxp  5184  rexxpf  5191  iunxpf  5192  cnvco  5230  dmiun  5255  dmuni  5256  dm0rn0  5263  brres  5323  dmres  5339  restidsing  5377  restidsingOLD  5378  cnvsym  5429  asymref  5431  codir  5435  qfto  5436  cnvopab  5452  cnvdif  5458  rniun  5462  dminss  5466  imainss  5467  difxp  5477  xpdifid  5481  dmsnn0  5518  cnvcnvsn  5530  cnvresima  5541  resco  5556  imaco  5557  rnco  5558  coiun  5562  coass  5571  ressn  5588  cnviin  5589  cnvpo  5590  cnvso  5591  xpco  5592  dflim2  5698  unisuc  5718  funcnv  5872  funcnv3  5873  fncnv  5876  fun11  5877  imadif  5887  fnres  5921  dfmpt3  5927  mptfnf  5928  fnopabg  5930  fint  5997  fin  5998  fores  6037  dff1o3  6056  f1ompt  6290  fsn  6308  imaiun  6407  isocnv2  6481  isocnv3  6482  isores2  6483  isomin  6487  eqoprab2b  6611  sucexb  6901  sucelon  6909  dflim4  6940  fun11iun  7019  f11o  7021  opabex3d  7037  opabex3  7038  dfopab2  7113  dfoprab3s  7114  fmpt2x  7125  fparlem1  7164  fparlem2  7165  fsplit  7169  suppvalbr  7186  tpostpos  7259  wfrlem8  7309  wfrfun  7312  dfsmo2  7331  brwitnlem  7474  oarec  7529  qsid  7700  uniinqs  7714  mapval2  7773  mapsncnv  7790  elixp2  7798  ixpin  7819  brsdom  7864  brdom2  7871  xpassen  7939  brsdom2  7969  unfilem1  8109  fiint  8122  dfsup2  8233  supmo  8241  eqinf  8273  infmo  8284  rankc1  8616  cp  8637  isinfcard  8798  aceq1  8823  aceq2  8825  dfac5lem3  8831  dfac10b  8844  dfac12a  8853  dffin7-2  9103  dfacfin7  9104  fin1a2lem6  9110  iunfo  9240  konigthlem  9269  axgroth6  9529  axgroth3  9532  sstskm  9543  ltexprlem1  9737  gt0srpr  9778  ltpsrpr  9809  map2psrpr  9810  ltresr  9840  fimaxre3  10849  sup3  10859  supaddc  10867  supmul1  10869  elnn0z  11267  elznn0nn  11268  zmin  11660  xrnemnf  11827  xrnepnf  11828  elioomnf  12139  elxrge0  12152  elfzuzb  12207  fzass4  12250  elfz2nn0  12300  elfzo2  12342  elfzo3  12355  lbfzo0  12375  fzind2  12448  nn0opthlem1  12917  cotr2g  13563  rexfiuz  13935  fsumcom2  14347  fsumcom2OLD  14348  prodmo  14505  fprodcom2  14553  fprodcom2OLD  14554  sinltx  14758  divalglem4  14957  divalglem10  14963  isprm2lem  15232  4sqlem12  15498  imasleval  16024  xpsfrnel  16046  xpscf  16049  isssc  16303  isffth2  16399  ispos2  16771  ismhm  17160  nsgacs  17453  isgim  17527  oppgcntz  17617  f1omvdco3  17692  pmtrprfvalrn  17731  efgrelexlemb  17986  pgpfac1  18302  pgpfac  18306  issrg  18330  opprsubg  18459  opprunit  18484  isirred2  18524  opprirred  18525  drngprop  18581  opprdrng  18594  islss  18756  islbs  18897  isdomn2  19120  unocv  19843  iunocv  19844  fvmptnn04if  20473  isbasis2g  20563  tgval2  20571  ntreq0  20691  isclo2  20702  cmpcov2  21003  is1stc2  21055  1stcelcls  21074  llyi  21087  unisngl  21140  txuni2  21178  xkobval  21199  hausdiag  21258  isfbas2  21449  elfg  21485  fbasrn  21498  fmfnfmlem3  21570  isfcls  21623  alexsubALTlem2  21662  istmd  21688  istgp  21691  istrg  21777  istdrg  21779  istdrg2  21791  isms2  22065  metuel2  22180  restmetu  22185  isngp  22210  isngp2  22211  isngp3  22212  elii1  22542  isncvsngp  22757  iscph  22778  isbn  22943  pmltpc  23026  ovolfcl  23042  finiunmbl  23119  iundisj  23123  dyaddisj  23170  vitalilem1  23182  vitalilem1OLD  23183  ellimc3  23449  ig1pval3  23738  plyun0  23757  plydivex  23856  aannenlem2  23888  ellogrn  24110  atandm  24403  atandm3  24405  atans2  24458  colinearalg  25590  axeuclid  25643  usgreg2spot  26594  h2hlm  27221  issh  27449  chcon2i  27707  chcon1i  27708  chcon3i  27709  chnlei  27728  cmcm2i  27836  cmcm3i  27837  3oalem3  27907  pjdifnormii  27926  pjneli  27966  dfadj2  28128  cnvadj  28135  hhcno  28147  hhcnf  28148  eleigvec  28200  eleigvec2  28201  pjimai  28419  isst  28456  ishst  28457  cvnbtwn4  28532  chrelat4i  28616  moel  28707  rmo3f  28719  rmo4fOLD  28720  rabid2f  28724  iunin1f  28757  iunxsngf  28758  disjnf  28766  cbvdisjf  28767  disjorf  28774  iundisjf  28784  disjexc  28788  dfrp2  28922  xrdifh  28932  iundisjfi  28942  xrnarchi  29069  isorng  29130  pmtrprfv2  29179  cmpcref  29245  ordtconlem1  29298  isrrext  29372  cntnevol  29618  ddemeas  29626  omssubaddlem  29688  omssubadd  29689  eulerpartleme  29752  eulerpartlemv  29753  eulerpartlemt0  29758  eulerpartlemgvv  29765  eulerpartlemn  29770  ballotlem2  29877  ballotlemodife  29886  bnj257  30026  bnj268  30028  bnj290  30029  bnj312  30031  bnj89  30041  bnj538OLD  30064  bnj887  30089  bnj976  30102  bnj1019  30104  bnj1146  30116  bnj1385  30157  bnj110  30182  bnj121  30194  bnj130  30198  bnj153  30204  bnj543  30217  bnj580  30237  bnj607  30240  bnj849  30249  bnj882  30250  bnj916  30257  bnj985  30277  bnj1033  30291  bnj1083  30300  bnj1090  30301  bnj1128  30312  bnj1174  30325  bnj1228  30333  erdszelem1  30427  cvmliftlem15  30534  snmlval  30567  elmpst  30687  mpstrcl  30692  untuni  30840  dfso3  30856  dftr6  30893  coep  30894  coepr  30895  dffr5  30896  dfso2  30897  dfpo2  30898  cnvco1  30903  cnvco2  30904  eldm3  30905  socnv  30908  dfdm5  30921  dfrn5  30922  frrlem5c  31030  elno3  31052  nofulllem5  31105  brsset  31166  idsset  31167  dfon3  31169  dfbigcup2  31176  dfom5b  31189  dffun10  31191  dfiota3  31200  fnimage  31206  brdomain  31210  brrange  31211  brimg  31214  brapply  31215  brcup  31216  brcap  31217  brsuccf  31218  funpartlem  31219  brrestrict  31226  dfrecs2  31227  brub  31231  altopelaltxp  31253  trer  31480  filnetlem4  31546  df3nandALT1  31566  imnand2  31569  bj-dfbi5  31729  bj-nfn  31795  bj-ssbssblem  31838  bj-ssbcom3lem  31839  bj-cbvex2v  31925  bj-equsalv  31931  bj-abeq1  31962  bj-vjust  31974  bj-sbnf  32016  bj-ralcom4  32062  bj-csbsnlem  32090  bj-restpw  32226  wl-nancom  32476  iundif1  32553  poimirlem25  32604  poimirlem26  32605  poimirlem30  32609  ismblfin  32620  mbfposadd  32627  itg2addnclem2  32632  ftc1anc  32663  inixp  32693  prdstotbnd  32763  heibor1lem  32778  isrngohom  32934  isidl  32983  isfldidl2  33038  isdmn3  33043  sbccom2lem  33099  pmapglbx  34073  lhpexle3  34316  cdleme25cv  34664  dicelval3  35487  diclspsn  35501  lcfls1c  35843  moxfr  36273  fphpd  36398  issdrg2  36787  ifpim1  36832  ifpnot  36833  ifpid2  36834  ifpim2  36835  ifpxorcor  36840  ifpnot23  36842  ifpananb  36870  ifpnannanb  36871  ifpxorxorb  36875  rp-fakeinunass  36880  undmrnresiss  36929  cnvssco  36931  cotrintab  36940  cnviun  36961  imaiun1  36962  coiun1  36963  elintima  36964  frege133d  37076  frege54cor0a  37177  or3or  37339  andi3or  37340  ntrneikb  37412  ntrneixb  37413  ntrneik4w  37418  k0004lem1  37465  undisjrab  37527  nzss  37538  pm10.541  37588  compab  37666  conss34OLD  37667  onfrALTlem5  37778  csbabgOLD  38072  eluni2f  38315  r19.32  39816  rmoanim  39828  upgrtrls  40909  upgristrl  40910  usgr2pth0  40971  iswwlks  41039  isclwwlks  41188  av-numclwwlkovf2  41515  issubmgm  41579  sgrp2sgrp  41654  islindeps  42036  elbigo  42143  setrec1lem3  42235  elpg  42256
  Copyright terms: Public domain W3C validator