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

Theorem 3bitr4i 306
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 281 . 2 (𝜑𝜃)
51, 4bitri 278 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 209
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 210
This theorem is referenced by:  bibi2d  346  pm4.71  561  pm5.32ri  579  an31  647  pm4.14  806  or4  924  orimdi  928  orbidi  950  ordi  1003  ordir  1004  andir  1006  dfbi3  1045  dfifp7  1065  ifpdfbi  1066  ifpn  1069  ifpnOLD  1070  3orrot  1089  3orcoma  1090  3ioran  1103  3ianor  1104  3anbi123i  1152  3orbi123i  1153  an6  1442  3or6  1444  an33rean  1480  an33reanOLD  1481  nancom  1487  xorcomOLD  1506  xorass  1507  xorbi12iOLD  1517  anxordi  1519  norcomOLD  1524  nornotOLD  1526  norass  1534  hadbi  1599  hadcoma  1600  hadcomaOLD  1601  hadcomb  1602  hadnot  1604  cador  1610  cadan  1611  cadcoma  1614  cadnot  1617  nic-axALT  1676  nfnbi  1856  19.26-3an  1873  19.43OLD  1884  19.32v  1941  19.31v  1942  19.42v  1954  4exdistr  1963  cbvexvw  2044  sbcom4  2099  sbcom3vv  2106  sbal  2166  excom  2169  19.32  2236  19.31  2237  19.42  2239  equsalv  2269  sbex  2289  sbanOLD  2313  sbor  2317  sbbi  2318  sbnvOLD  2323  sbanvOLD  2327  sbbivOLD  2328  cbvexv1  2363  cbvex2v  2366  eeeanv  2372  sbnf2  2378  cbvex2  2435  equsal  2440  dfsb3  2533  dfsb3ALT  2592  sbanALT  2610  sbbiALT  2611  mo4  2649  eu6  2658  eubii  2669  dfeu  2680  sb8eulem  2683  sb8mo  2686  cbvmow  2687  cbvmowOLD  2688  cbveuw  2690  cbveuALT  2693  eu1  2695  sbmo  2699  cbvabv  2890  cbvabw  2891  cbvabwOLD  2892  cbvab  2893  abeq1  2947  nfceqi  2976  sbabel  3010  ralbii2  3155  r19.21v  3167  r2allem  3190  ralcom4  3223  rexbii2  3233  rexanidOLD  3241  reuanid  3313  rmoanid  3314  r19.32v  3322  r19.41v  3328  r19.41  3329  r19.42v  3331  r19.43  3332  ralcom  3335  rexcomOLD  3337  ralcomf  3338  rexcomf  3339  reeanlem  3346  3reeanv  3349  2ralor  3350  rabid2  3362  rabid2f  3363  rabbi  3364  reubiia  3371  rmobiia  3376  reu5  3403  rmo5  3407  cbvralfw  3410  cbvralfwOLD  3411  cbvrexfw  3412  cbvralf  3413  cbvrexf  3414  cbvreuw  3417  cbvrmow  3418  cbvrmowOLD  3419  cbvreu  3422  cbvrmo  3423  cbvralvw  3424  cbvrexvw  3425  vjust  3470  abv  3479  ceqsex3v  3520  ceqsex4v  3521  ceqsex8v  3523  eueq  3674  reu2  3691  reu6  3692  reu3  3693  rmo4  3696  rmo3f  3700  2reu5  3724  cbvsbcw  3779  cbvsbc  3781  sbccomlem  3826  rmo3  3845  rmoanim  3850  rmoanimALT  3851  cbvralcsf  3897  cbvrexcsf  3898  cbvreucsf  3899  dfss2  3928  eqss  3957  uniiunlem  4036  sspsstri  4054  compleq  4099  ssequn1  4131  unss  4135  rexun  4141  ralunb  4142  elin3  4151  incomOLD  4153  inass  4170  ssin  4181  elsymdif  4198  nssinpss  4207  dfun2  4210  difin  4212  indi  4224  indifdir  4234  ssdif0  4295  inssdif0  4301  rabeq0  4310  disj3  4375  ssundif  4405  dfif2  4441  eldifpr  4571  rexsns  4583  snprc  4627  reusn  4637  difsnpss  4713  tpss  4741  pwpr  4807  eluni2  4817  elunirab  4829  uniun  4836  unissb  4845  elintrab  4863  ssintrab  4874  intun  4883  intpr  4884  iuncom  4901  iuncom4  4902  iunab  4950  ssiinf  4953  iunn0  4964  iinab  4965  iunin2  4968  iinun2  4970  iundif2  4971  iunun  4990  iunxun  4991  iunxiun  4994  sspwuni  4997  iinpw  5003  cbvdisj  5017  disjor  5022  brun  5093  brin  5094  brdif  5095  dftr2  5150  intexrab  5219  inuni  5222  ssext  5324  pweqb  5326  otth2  5352  propeqop  5374  opelopabsbALT  5393  eqopab2bw  5412  eqopab2b  5416  pwin  5431  pwun  5435  elxp2  5556  xpiundi  5599  xpiundir  5600  poinxp  5609  soinxp  5610  frinxp  5611  seinxp  5612  weinxp  5613  inopab  5678  difopab  5679  raliunxp  5687  rexiunxp  5688  rexxpf  5695  iunxpf  5696  cnvco  5733  dmiun  5759  dmuni  5760  dm0rn0  5772  dmres  5853  restidsing  5900  cnvsym  5952  asymref  5954  codir  5958  qfto  5959  cnvopab  5975  cnvdif  5980  rniun  5984  dminss  5988  imainss  5989  difxp  5999  xpdifid  6003  dmsnn0  6042  cnvcnvsn  6054  cnvresima  6065  resco  6081  imaco  6082  rnco  6083  coiun  6087  coass  6096  ressn  6114  cnviin  6115  cnvpo  6116  cnvso  6117  xpco  6118  opreu2reurex  6123  dflim2  6225  unisuc  6245  funcnv  6402  funcnv3  6403  fncnv  6406  fun11  6407  imadif  6417  fnres  6454  dfmpt3  6462  mptfnf  6463  fnopabg  6465  fint  6539  fin  6540  fores  6582  dff1o3  6603  f1ompt  6857  fsn  6879  imaiun  6987  isocnv2  7068  isocnv3  7069  isores2  7070  isomin  7074  eqoprab2bw  7208  eqoprab2b  7209  elpwpwel  7474  sucexb  7509  sucelon  7517  dflim4  7548  fiun  7630  f1iun  7631  f11o  7634  opabex3d  7652  opabex3rd  7653  opabex3  7654  dfopab2  7736  dfoprab3s  7737  fmpox  7751  fparlem1  7794  fparlem2  7795  fsplitOLD  7800  suppvalbr  7821  tpostpos  7899  wfrlem8  7949  wfrfun  7952  dfsmo2  7971  brwitnlem  8119  oarec  8175  qsid  8350  uniinqs  8364  mapval2  8423  mapsncnv  8444  elixp2  8452  ixpin  8474  brsdom  8519  brdom2  8526  xpassen  8598  brsdom2  8629  unfilem1  8770  fiint  8783  dfsup2  8896  supmo  8904  eqinf  8936  infmo  8947  rankc1  9287  cp  9308  isinfcard  9507  aceq1  9532  aceq2  9534  dfac5lem3  9540  dfac10b  9554  dfac12a  9563  dffin7-2  9809  dfacfin7  9810  fin1a2lem6  9816  iunfo  9950  konigthlem  9979  axgroth6  10239  axgroth3  10242  sstskm  10253  ltexprlem1  10447  gt0srpr  10489  ltpsrpr  10520  map2psrpr  10521  ltresr  10551  fimaxre3  11575  sup3  11585  supaddc  11595  supmul1  11597  elnn0z  11982  elznn0nn  11983  zmin  12332  xrnemnf  12500  xrnepnf  12501  elioomnf  12822  elxrge0  12835  elfzuzb  12896  fzass4  12940  elfz2nn0  12993  elfzo2  13036  elfzo3  13049  lbfzo0  13072  fzind2  13150  nn0opthlem1  13624  hashgt23el  13781  cotr2g  14327  rexfiuz  14698  fsumcom2  15120  prodmo  15281  fprodcom2  15329  sinltx  15533  divalglem4  15736  divalglem10  15742  4sqlem12  16281  imasleval  16805  xpsfrnel  16826  xpscf  16829  isssc  17081  isffth2  17177  ispos2  17549  ismhm  17949  issubmndb  17961  nsgacs  18305  isgim  18393  oppgcntz  18483  f1omvdco3  18568  pmtrprfvalrn  18607  efgrelexlemb  18867  pgpfac1  19193  pgpfac  19197  issrg  19248  opprsubg  19380  opprunit  19405  isirred2  19445  opprirred  19446  drngprop  19504  opprdrng  19517  issdrg2  19568  islss  19697  islbs  19839  isdomn2  20063  unocv  20367  iunocv  20368  isbasis2g  21551  tgval2  21559  ntreq0  21680  isclo2  21691  cmpcov2  21993  is1stc2  22045  1stcelcls  22064  llyi  22077  unisngl  22130  txuni2  22168  xkobval  22189  hausdiag  22248  isfbas2  22438  elfg  22474  fbasrn  22487  fmfnfmlem3  22559  isfcls  22612  alexsubALTlem2  22651  istmd  22677  istgp  22680  istrg  22767  istdrg  22769  istdrg2  22781  isms2  23055  metuel2  23170  restmetu  23175  isngp  23200  isngp2  23201  isngp3  23202  elii1  23538  isncvsngp  23752  iscph  23773  isbn  23940  pmltpc  24052  ovolfcl  24068  finiunmbl  24146  iundisj  24150  dyaddisj  24198  vitalilem1  24210  ellimc3  24480  ig1pval3  24773  plyun0  24792  plydivex  24891  aannenlem2  24923  ellogrn  25149  atandm  25460  atandm3  25462  atans2  25515  tgjustf  26265  colinearalg  26702  axeuclid  26755  nbgrsym  27151  upgrtrls  27489  upgristrl  27490  usgr2pth0  27552  iswwlks  27620  isclwwlk  27767  clwwlkneq0  27812  h2hlm  28761  issh  28989  chcon2i  29245  chcon1i  29246  chcon3i  29247  chnlei  29266  cmcm2i  29374  cmcm3i  29375  3oalem3  29445  pjdifnormii  29464  pjneli  29504  dfadj2  29666  cnvadj  29673  hhcno  29685  hhcnf  29686  eleigvec  29738  eleigvec2  29739  pjimai  29957  isst  29994  ishst  29995  cvnbtwn4  30070  chrelat4i  30154  2reucom  30248  moel  30257  reuxfrdf  30260  difrab2  30266  inpr0  30299  iunin1f  30316  disjnf  30328  cbvdisjf  30329  disjorf  30337  iundisjf  30347  disjexc  30351  dfrp2  30501  xrdifh  30513  iundisjfi  30529  hashxpe  30539  pmtrprfv2  30763  xrnarchi  30844  isorng  30904  ccfldextdgrr  31114  cmpcref  31172  ordtconnlem1  31241  isrrext  31315  cntnevol  31561  ddemeas  31569  omssubaddlem  31631  omssubadd  31632  eulerpartleme  31695  eulerpartlemv  31696  eulerpartlemt0  31701  eulerpartlemgvv  31708  eulerpartlemn  31713  ballotlem2  31820  ballotlemodife  31829  oddprm2  32000  bnj257  32051  bnj268  32053  bnj290  32054  bnj312  32056  bnj89  32065  bnj887  32110  bnj976  32123  bnj1019  32125  bnj1146  32137  bnj1385  32178  bnj110  32204  bnj121  32216  bnj130  32220  bnj153  32226  bnj543  32239  bnj580  32259  bnj607  32262  bnj849  32271  bnj882  32272  bnj916  32279  bnj985v  32299  bnj985  32300  bnj1033  32315  bnj1083  32324  bnj1090  32325  bnj1128  32336  bnj1174  32349  bnj1228  32357  erdszelem1  32512  cvmliftlem15  32619  snmlval  32652  satfvsuclem2  32681  satfdm  32690  elmpst  32857  mpstrcl  32862  untuni  33009  dfso3  33024  dftr6  33060  coep  33061  coepr  33062  dffr5  33063  dfso2  33064  dfpo2  33065  cnvco1  33069  cnvco2  33070  eldm3  33071  dfdm5  33090  dfrn5  33091  imaindm  33096  frrlem9  33205  elno3  33236  conway  33338  madeval2  33364  brsset  33424  idsset  33425  dfon3  33427  dfbigcup2  33434  dfom5b  33447  dffun10  33449  dfiota3  33458  fnimage  33464  brdomain  33468  brrange  33469  brimg  33472  brapply  33473  brcup  33474  brcap  33475  brsuccf  33476  funpartlem  33477  brrestrict  33484  dfrecs2  33485  brub  33489  altopelaltxp  33511  trer  33738  filnetlem4  33803  df3nandALT1  33821  imnand2  33824  bj-dfbi5  33981  bj-bixor  33999  bj-nnfnt  34145  bj-sbnf  34240  bj-csbsnlem  34305  bj-rcleqf  34422  bj-sscon  34426  bj-pw0ALT  34427  bj-restpw  34468  bj-opelidb1  34529  bj-imdiridlem  34561  bj-imdirco  34566  wl-df3xor2  34845  wl-3xorrot  34853  wl-3xorcoma  34854  wl-3xornot  34857  wl-df2-3mintru2  34861  wl-df3-3mintru2  34862  wl-df4-3mintru2  34863  wl-equsalvw  34901  wl-dfrexv  34972  wl-dfrexex  34973  wl-dfrmosb  34976  wl-dfrmov  34977  wl-dfreusb  34980  wl-dfreuv  34981  wl-dfrabv  34985  iundif1  34989  poimirlem25  35040  poimirlem26  35041  poimirlem30  35045  ismblfin  35056  mbfposadd  35062  itg2addnclem2  35067  ftc1anc  35096  inixp  35124  prdstotbnd  35190  heibor1lem  35205  isrngohom  35361  isidl  35410  isfldidl2  35465  isdmn3  35470  sbccom2lem  35520  triantru3  35618  vvdifopab  35639  brres2  35647  eldmqsres  35661  inxpss  35687  n0el2  35708  trcoss2  35842  dfeqvrel2  35943  dfeqvrel3  35944  redundeq1  35982  redundpbi1  35984  refrelredund4  35988  funALTVfun  36049  dfeldisj3  36070  dfeldisj5  36072  pmapglbx  37023  lhpexle3  37266  cdleme25cv  37612  dicelval3  38434  diclspsn  38448  lcfls1c  38790  sn-axrep5v  39349  psspwb  39355  moxfr  39563  fphpd  39687  ifpim1  40107  ifpnot  40108  ifpid2  40109  ifpim2  40110  ifpxorcor  40114  ifpnot23  40116  ifpananb  40144  ifpnannanb  40145  ifpxorxorb  40149  rp-fakeinunass  40153  snen1g  40162  pren2  40182  alephiso2  40187  undmrnresiss  40234  cnvssco  40236  cotrintab  40244  cnviun  40281  imaiun1  40282  coiun1  40283  elintima  40284  frege133d  40396  frege54cor0a  40495  or3or  40657  andi3or  40658  ntrneik4w  40736  k0004lem1  40783  ismnuprim  40936  undisjrab  40944  nzss  40955  pm10.541  41005  compab  41080  onfrALTlem5  41182  onfrALTlem5VD  41525  inn0f  41641  eluni2f  41675  euabsneu  43559  aiotaexb  43585  aiotavb  43586  r19.32  43592  3an4ancom24  43764  ichn  43912  ichcom  43915  ichbi12i  43916  prproropf1olem0  43958  pairreueq  43966  issubmgm  44348  sgrp2sgrp  44427  islindeps  44801  elbigo  44904  setrec1lem3  45158  elpg  45182
  Copyright terms: Public domain W3C validator