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

Theorem 3bitr4i 294
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 269 . 2 (𝜑𝜃)
51, 4bitri 266 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  bibi2d  333  pm4.71  549  pm5.32ri  567  an31  630  an4  638  pm4.14  832  or4  941  orimdi  945  orbidi  966  ordi  1019  ordir  1020  andir  1022  dfbi3  1063  dfbi3OLD  1064  dfifp7  1085  ifpn  1088  3orrot  1105  3orcoma  1106  3orcombOLD  1108  3ancomaOLD  1113  3anrotOLD  1117  3ioran  1124  3ianor  1125  3anbi123i  1187  3orbi123i  1188  an6  1562  3or6  1564  an33rean  1600  xorcom  1621  xorass  1622  xorbi12i  1631  anxordi  1633  hadbi  1692  hadcoma  1693  hadcomb  1694  hadnot  1696  cador  1702  cadan  1703  cadcoma  1706  cadnot  1709  nic-axALT  1754  nfnbi  1943  nfnbiOLD  1944  19.26-3an  1964  19.26-3anOLD  1965  19.43OLD  1976  nfbiiOLD  2001  19.32v  2034  19.31v  2035  19.42v  2046  4exdistr  2052  sbequ8  2067  equsalvw  2102  cbvexvw  2139  excom  2211  19.32  2271  19.31  2272  19.42  2275  equsalv  2278  equsalhwOLD  2301  cbvexv1  2351  eeeanv  2359  cbvex2  2453  equsal  2460  dfsb3  2535  sbor  2559  sban  2560  sbbi  2562  sbnf2  2603  sbcom4  2608  sbex  2625  eu5  2658  sb8eu  2666  sb8mo  2667  cbvmo  2669  eu1  2673  sbmo  2678  abeq1  2916  cbvab  2929  sbabel  2976  rexanid  3106  reuanid  3107  rmoanid  3108  r2allem  3124  r19.21v  3147  ralbii2  3165  rexbii2  3226  r19.30  3269  r19.32v  3270  r19.41v  3276  r19.41  3277  r19.42v  3279  r19.43  3280  ralcomf  3283  rexcomf  3284  reean  3293  3reeanv  3295  2ralor  3296  rabid2  3306  rabid2f  3307  rabbi  3308  reubiia  3315  rmobiia  3320  reu5  3347  rmo5  3350  cbvralf  3353  cbvrexf  3354  cbvreu  3357  cbvrmo  3358  vjust  3391  abv  3399  ceqsex3v  3439  ceqsex4v  3440  ceqsex8v  3442  eueq  3573  reu2  3589  reu6  3590  reu3  3591  rmo4  3594  2reu5  3611  cbvsbc  3659  sbccomlem  3701  rmo3  3720  cbvralcsf  3757  cbvrexcsf  3758  cbvreucsf  3759  eqss  3810  uniiunlem  3886  sspsstri  3904  compleq  3948  ssequn1  3979  unss  3983  rexun  3989  ralunb  3990  elin3  4000  incom  4001  inass  4017  ssin  4028  elsymdif  4044  symdifassOLD  4049  symdif2OLD  4052  nssinpss  4055  dfun2  4058  difin  4060  indi  4072  indifdir  4082  ssdif0  4140  inssdif0  4145  dfnf5  4150  rabeq0  4154  disj3  4215  ssundif  4245  dfif2  4278  eldifpr  4395  rexsns  4407  snprc  4441  reusn  4450  difsnpss  4525  tpss  4553  preqsnOLD  4580  pwpr  4620  eluni2  4630  elunirab  4638  uniun  4647  unissb  4659  elintrab  4677  ssintrab  4688  intun  4697  intpr  4698  iuncom  4715  iuncom4  4716  iunab  4754  ssiinf  4757  iunn0  4768  iinab  4769  iunin2  4772  iinun2  4774  iundif2  4775  iunun  4792  iunxun  4793  iunxiun  4796  sspwuni  4799  iinpw  4805  cbvdisj  4818  disjor  4822  brun  4891  brin  4892  brdif  4893  dftr2  4944  intexrab  5012  inuni  5015  ssext  5110  pweqb  5112  otth2  5138  snopeqopOLD  5158  propeqop  5159  opelopabsbALT  5176  eqopab2b  5197  pwin  5210  pwun  5214  elxp2  5331  xpiundi  5370  xpiundir  5371  poinxp  5381  soinxp  5382  frinxp  5383  seinxp  5384  weinxp  5385  inopab  5451  difopab  5452  raliunxp  5460  rexiunxp  5461  rexxpf  5468  iunxpf  5469  cnvco  5506  dmiun  5531  dmuni  5532  dm0rn0  5540  brresOLD  5605  dmres  5619  restidsing  5667  cnvsym  5718  asymref  5720  codir  5724  qfto  5725  cnvopab  5741  cnvdif  5747  rniun  5751  dminss  5755  imainss  5756  difxp  5766  xpdifid  5770  dmsnn0  5808  cnvcnvsn  5821  cnvresima  5834  resco  5850  imaco  5851  rnco  5852  coiun  5856  coass  5865  ressn  5882  cnviin  5883  cnvpo  5884  cnvso  5885  xpco  5886  dflim2  5991  unisuc  6011  funcnv  6166  funcnv3  6167  fncnv  6170  fun11  6171  imadif  6181  fnres  6215  dfmpt3  6222  mptfnf  6223  fnopabg  6225  fint  6296  fin  6297  fores  6337  dff1o3  6356  f1ompt  6600  fsn  6622  imaiun  6724  isocnv2  6802  isocnv3  6803  isores2  6804  isomin  6808  eqoprab2b  6940  sucexb  7236  sucelon  7244  dflim4  7275  fun11iun  7353  f11o  7355  opabex3d  7372  opabex3  7373  dfopab2  7451  dfoprab3s  7452  fmpt2x  7466  fparlem1  7508  fparlem2  7509  fsplit  7513  suppvalbr  7530  tpostpos  7604  wfrlem8  7655  wfrfun  7658  dfsmo2  7677  brwitnlem  7821  oarec  7876  qsid  8045  uniinqs  8059  mapval2  8119  mapsncnv  8138  elixp2  8146  ixpin  8167  brsdom  8212  brdom2  8219  xpassen  8290  brsdom2  8320  unfilem1  8460  fiint  8473  dfsup2  8586  supmo  8594  eqinf  8626  infmo  8637  rankc1  8977  cp  8998  isinfcard  9195  aceq1  9220  aceq2  9222  dfac5lem3  9228  dfac10b  9243  dfac12a  9252  dffin7-2  9502  dfacfin7  9503  fin1a2lem6  9509  iunfo  9643  konigthlem  9672  axgroth6  9932  axgroth3  9935  sstskm  9946  ltexprlem1  10140  gt0srpr  10181  ltpsrpr  10212  map2psrpr  10213  ltresr  10243  fimaxre3  11252  sup3  11262  supaddc  11272  supmul1  11274  elnn0z  11652  elznn0nn  11653  zmin  11999  xrnemnf  12163  xrnepnf  12164  elioomnf  12483  elxrge0  12497  elfzuzb  12555  fzass4  12598  elfz2nn0  12650  elfzo2  12693  elfzo3  12706  lbfzo0  12728  fzind2  12806  nn0opthlem1  13271  cotr2g  13936  rexfiuz  14306  fsumcom2  14724  prodmo  14883  fprodcom2  14931  sinltx  15135  divalglem4  15335  divalglem10  15341  4sqlem12  15873  imasleval  16402  xpsfrnel  16424  xpscf  16427  isssc  16680  isffth2  16776  ispos2  17149  ismhm  17538  nsgacs  17828  isgim  17902  oppgcntz  17991  f1omvdco3  18066  pmtrprfvalrn  18105  efgrelexlemb  18360  pgpfac1  18677  pgpfac  18681  issrg  18705  opprsubg  18834  opprunit  18859  isirred2  18899  opprirred  18900  drngprop  18958  opprdrng  18971  islss  19135  islbs  19279  isdomn2  19504  unocv  20230  iunocv  20231  fvmptnn04if  20863  isbasis2g  20962  tgval2  20970  ntreq0  21091  isclo2  21102  cmpcov2  21403  is1stc2  21455  1stcelcls  21474  llyi  21487  unisngl  21540  txuni2  21578  xkobval  21599  hausdiag  21658  isfbas2  21848  elfg  21884  fbasrn  21897  fmfnfmlem3  21969  isfcls  22022  alexsubALTlem2  22061  istmd  22087  istgp  22090  istrg  22176  istdrg  22178  istdrg2  22190  isms2  22464  metuel2  22579  restmetu  22584  isngp  22609  isngp2  22610  isngp3  22611  elii1  22943  isncvsngp  23157  iscph  23178  isbn  23343  pmltpc  23427  ovolfcl  23443  finiunmbl  23521  iundisj  23525  dyaddisj  23573  vitalilem1  23585  ellimc3  23853  ig1pval3  24144  plyun0  24163  plydivex  24262  aannenlem2  24294  ellogrn  24516  atandm  24813  atandm3  24815  atans2  24868  colinearalg  26000  axeuclid  26053  nbgrsym  26475  upgrtrls  26822  upgristrl  26823  usgr2pth0  26885  iswwlks  26953  isclwwlk  27123  clwwlkneq0  27172  h2hlm  28162  issh  28390  chcon2i  28648  chcon1i  28649  chcon3i  28650  chnlei  28669  cmcm2i  28777  cmcm3i  28778  3oalem3  28848  pjdifnormii  28867  pjneli  28907  dfadj2  29069  cnvadj  29076  hhcno  29088  hhcnf  29089  eleigvec  29141  eleigvec2  29142  pjimai  29360  isst  29397  ishst  29398  cvnbtwn4  29473  chrelat4i  29557  moel  29648  rmo3f  29658  rmo4fOLD  29659  difrab2  29661  iunin1f  29696  disjnf  29706  cbvdisjf  29707  disjorf  29714  iundisjf  29724  disjexc  29728  dfrp2  29856  xrdifh  29866  iundisjfi  29879  xrnarchi  30060  isorng  30121  pmtrprfv2  30170  cmpcref  30239  ordtconnlem1  30292  isrrext  30366  cntnevol  30613  ddemeas  30621  omssubaddlem  30683  omssubadd  30684  eulerpartleme  30747  eulerpartlemv  30748  eulerpartlemt0  30753  eulerpartlemgvv  30760  eulerpartlemn  30765  ballotlem2  30872  ballotlemodife  30881  oddprm2  31055  bnj257  31095  bnj268  31097  bnj290  31098  bnj312  31100  bnj89  31109  bnj538OLD  31130  bnj887  31155  bnj976  31168  bnj1019  31170  bnj1146  31182  bnj1385  31223  bnj110  31248  bnj121  31260  bnj130  31264  bnj153  31270  bnj543  31283  bnj580  31303  bnj607  31306  bnj849  31315  bnj882  31316  bnj916  31323  bnj985  31343  bnj1033  31357  bnj1083  31366  bnj1090  31367  bnj1128  31378  bnj1174  31391  bnj1228  31399  erdszelem1  31493  cvmliftlem15  31600  snmlval  31633  elmpst  31753  mpstrcl  31758  untuni  31905  dfso3  31920  dftr6  31959  coep  31960  coepr  31961  dffr5  31962  dfso2  31963  dfpo2  31964  cnvco1  31968  cnvco2  31969  eldm3  31970  dfdm5  31993  dfrn5  31994  imaindm  31999  frrlem5c  32104  elno3  32126  conway  32228  madeval2  32254  brsset  32314  idsset  32315  dfon3  32317  dfbigcup2  32324  dfom5b  32337  dffun10  32339  dfiota3  32348  fnimage  32354  brdomain  32358  brrange  32359  brimg  32362  brapply  32363  brcup  32364  brcap  32365  brsuccf  32366  funpartlem  32367  brrestrict  32374  dfrecs2  32375  brub  32379  altopelaltxp  32401  trer  32628  filnetlem4  32694  df3nandALT1  32712  imnand2  32715  bj-dfbi5  32870  bj-ssbssblem  32961  bj-ssbcom3lem  32962  bj-cbvex2v  33049  bj-abeq1  33085  bj-vjust  33097  bj-sbnf  33138  bj-ralcom4  33173  bj-csbsnlem  33203  bj-sscon  33321  bj-restpw  33353  wl-nancom  33610  iundif1  33693  poimirlem25  33744  poimirlem26  33745  poimirlem30  33749  ismblfin  33760  mbfposadd  33766  itg2addnclem2  33771  ftc1anc  33802  inixp  33832  prdstotbnd  33901  heibor1lem  33916  isrngohom  34072  isidl  34121  isfldidl2  34176  isdmn3  34181  sbccom2lem  34236  triantru3  34318  vvdifopab  34339  brres2  34349  eldmqsres  34365  inxpss  34395  n0el2  34415  trcoss2  34544  pmapglbx  35546  lhpexle3  35789  cdleme25cv  36136  dicelval3  36958  diclspsn  36972  lcfls1c  37314  psspwb  37749  moxfr  37754  fphpd  37879  issdrg2  38266  ifpim1  38310  ifpnot  38311  ifpid2  38312  ifpim2  38313  ifpxorcor  38318  ifpnot23  38320  ifpananb  38348  ifpnannanb  38349  ifpxorxorb  38353  rp-fakeinunass  38358  undmrnresiss  38407  cnvssco  38409  cotrintab  38418  cnviun  38439  imaiun1  38440  coiun1  38441  elintima  38442  frege133d  38554  frege54cor0a  38654  or3or  38816  andi3or  38817  ntrneikb  38889  ntrneixb  38890  ntrneik4w  38895  k0004lem1  38942  undisjrab  39002  nzss  39013  pm10.541  39063  compab  39141  onfrALTlem5  39252  csbabgOLD  39544  onfrALTlem5VD  39612  inn0f  39732  eluni2f  39775  aiotaexb  41670  aiotavb  41671  r19.32  41677  rmoanim  41688  3an4ancom24  41855  issubmgm  42354  sgrp2sgrp  42429  islindeps  42807  elbigo  42910  setrec1lem3  43001  elpg  43025
  Copyright terms: Public domain W3C validator