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

Theorem 3bitri 298
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
3bitri.1 (𝜑𝜓)
3bitri.2 (𝜓𝜒)
3bitri.3 (𝜒𝜃)
Assertion
Ref Expression
3bitri (𝜑𝜃)

Proof of Theorem 3bitri
StepHypRef Expression
1 3bitri.1 . 2 (𝜑𝜓)
2 3bitri.2 . . 3 (𝜓𝜒)
3 3bitri.3 . . 3 (𝜒𝜃)
42, 3bitri 276 . 2 (𝜓𝜃)
51, 4bitri 276 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  bibi1i  340  pm5.32  574  biadan  815  orbi1i  907  orass  915  or32  919  cases  1034  3anidm  1096  an3andi  1473  an33rean  1474  nanbi  1484  excxor  1500  norassOLD  1525  cadan  1601  cadcomb  1605  nic-axALT  1666  tbw-bijust  1690  rb-bijust  1741  nf2  1777  19.43  1874  19.43OLD  1875  3exdistr  1953  19.12vvv  1986  sb3an  2078  equsb3rOLD  2102  sbcom2  2158  excom13  2161  sbco4  2276  sbn  2279  19.12vv  2360  eeeanv  2363  ee4anv  2364  2sb8ev  2367  2sb8evOLD  2368  sbel2x  2494  sbnOLD  2537  2sb8e  2572  sbnALT  2591  dfmo  2678  sb8eulem  2680  2mo2  2728  2eu7  2741  2eu8  2742  r19.26-3  3172  r19.23v  3279  rexcom  3355  ralcom13  3359  rexcom13  3360  cbvreuw  3444  cbvreu  3448  ceqsralt  3529  ceqsex2  3544  ceqsex2v  3545  ceqsex4v  3547  ralrab2  3689  rexrab2  3692  reu2  3715  rmo4  3720  reu8  3723  rmo3f  3724  2reu5lem3  3747  sbc3an  3837  reu8nf  3859  rmo2  3869  rmo3  3871  rmo3OLD  3872  rmoanim  3877  dfss2  3954  ss2rab  4046  rabss  4047  ssrab  4048  dfdif3  4090  symdifass  4227  dfss4  4234  undi  4250  undif3  4264  difin2  4265  dfnul2OLD  4293  difin0ss  4327  disj  4397  disj4  4406  rabsssn  4599  disjsn  4641  raldifsni  4722  ssunpr  4759  sspr  4760  sstp  4761  uni0b  4857  uni0c  4858  ssint  4885  iunss  4961  iundif2  4988  disjor  5038  nfnid  5268  reusv2lem4  5293  ssextss  5338  exss  5347  eqvinop  5370  sbcop  5372  opcom  5383  opeqpr  5387  brabsb  5410  opelopabf  5424  dfid3  5456  pofun  5485  opeliunxp  5613  xpiundi  5616  brinxp2  5623  reliun  5683  exopxfr  5708  cnvuni  5751  dmopab3  5782  rnep  5791  elres  5885  elsnres  5886  elrid  5907  asymref2  5971  intirr  5972  xpeq0  6011  xpdifid  6019  ssrnres  6029  dminxp  6031  dfrel4v  6041  elid  6050  dmsnn0  6058  rnco  6099  coeq0  6102  sspred  6150  wfi  6175  sb8iota  6319  dffun2  6359  fun11  6422  isarep1  6436  dff1o4  6617  opabiota  6740  fvopab5  6793  eqfnfv3  6797  fvn0ssdmfun  6835  fnressn  6913  f13dfv  7022  dff1o6  7023  fliftel  7051  oprabidw  7176  oprabid  7177  mpo2eqb  7272  ralrnmpo  7278  uniuni  7472  dflim3  7550  dfom2  7570  elxp4  7615  elxp5  7616  opabex3d  7657  opabex3rd  7658  opabex3  7659  el2xptp  7726  fsplit  7803  xporderlem  7812  dfrecs3  8000  tz7.48lem  8068  seqomlem2  8078  oaord  8163  oeeu  8219  nnaord  8235  ecid  8352  mptelixpg  8488  elixpsn  8490  xpsnen  8590  xpcomco  8596  xpassen  8600  omxpenlem  8607  dom0  8634  modom  8708  tz9.12lem3  9207  rankxpsuc  9300  cp  9309  cardprclem  9397  infxpenlem  9428  dfac5lem1  9538  dfac5lem2  9539  dfac5lem5  9542  dfac10c  9553  kmlem3  9567  kmlem12  9576  kmlem13  9577  kmlem14  9578  kmlem15  9579  ackbij2  9654  cf0  9662  cflim2  9674  dffin7-2  9809  dfacfin7  9810  fin1a2lem12  9822  axdc3lem3  9863  cfpwsdom  9995  recmulnq  10375  genpass  10420  psslinpr  10442  suplem2pr  10464  opelreal  10541  ltxrlt  10700  addid1  10809  fimaxreOLD  11574  elnn0  11888  elxnn0  11958  elnn0z  11983  nnwos  12304  elxr  12501  xrnepnf  12503  elfzuzb  12892  4fvwrd4  13017  preduz  13019  elfzo2  13031  ssnn0fi  13343  sqeqori  13566  xpcogend  14324  cotr2g  14326  fsumcom2  15119  modfsummod  15139  fprodcom2  15328  rpnnen2lem12  15568  gcdcllem1  15838  isprm2  16016  isprm7  16042  pythagtriplem2  16144  infpn2  16239  4sqlem12  16282  initoid  17255  termoid  17256  eldmcoa  17315  oduposb  17736  gsumwspan  18001  isnsg2  18248  isnsg4  18259  cycsubmel  18283  efgcpbllemb  18812  dmdprd  19051  dprdval  19056  dprdw  19063  dprd2d2  19097  dfrhm2  19400  brric2  19431  issubrg  19466  islmim  19765  lbsextlem2  19862  opsrtoslem1  20194  cnfldfunALT  20488  pjfval2  20783  ntreq0  21615  cmpcov2  21928  cmpsub  21938  2ndcdisj  21994  unisngl  22065  txbas  22105  elpt  22110  txkgen  22190  xkococn  22198  fbun  22378  trfil2  22425  fin1aufil  22470  alexsubALTlem3  22587  cnextcn  22605  qustgplem  22658  eltsms  22670  ustn0  22758  fmucndlem  22829  metrest  23063  restmetu  23109  isclmp  23630  srabn  23892  ellogdm  25149  1cubr  25347  leibpilem2  25447  dmarea  25463  vmasum  25720  dchrelbas2  25741  2lgslem4  25910  tgcgr4  26245  ltgov  26311  axlowdimlem13  26668  axeuclidlem  26676  numedglnl  26857  nbupgrres  27074  vtxd0nedgb  27198  rusgrprc  27300  usgr2pth0  27474  wspthsnwspthsnon  27623  isclwwlk  27690  clwwlkn1  27747  clwwlkn2  27750  clwwlknonel  27802  3pthdlem1  27871  iseupthf1o  27909  frgr3v  27982  fusgr2wsp2nb  28041  frgrregord013  28102  h2hcau  28684  h2hlm  28685  shlesb1i  29091  shne0i  29153  chnlei  29190  cmbr2i  29301  pjneli  29428  ho02i  29534  adjsym  29538  adjeu  29594  lnopeqi  29713  largei  29972  atoml2i  30088  cdj3lem3b  30145  or3di  30153  mo5f  30181  dmrab  30188  disjnf  30249  disjorf  30258  ssrelf  30295  ofpreima  30339  disjdsct  30365  1stpreima  30369  2ndpreima  30370  f1od2  30384  xrdifh  30430  nndiffz1  30436  ordtconnlem1  31067  ind1a  31178  measiuns  31376  elunirnmbfm  31411  eulerpartlemr  31532  eulerpartlemgh  31536  eulerpartlemn  31539  ballotlemodife  31655  bnj250  31871  bnj334  31883  bnj345  31884  bnj89  31891  bnj115  31895  bnj919  31938  bnj1304  31991  bnj92  32034  bnj124  32043  bnj126  32045  bnj154  32050  bnj155  32051  bnj523  32059  bnj526  32060  bnj540  32064  bnj581  32080  bnj916  32105  bnj929  32108  bnj964  32115  bnj978  32121  bnj983  32123  bnj1039  32141  bnj1040  32142  bnj1123  32156  bnj1128  32160  bnj1398  32204  lfuhgr3  32264  cvmlift2lem1  32447  satfv0  32503  satf0  32517  satf0op  32522  satffunlem  32546  satffunlem1lem1  32547  satffunlem2lem1  32549  elmthm  32721  quad3  32811  3orit  32843  brtp  32883  dftr6  32884  dfpo2  32889  eldm3  32895  elrn3  32896  elima4  32917  19.12b  32944  frpoind  32978  frind  32983  nosupbnd1lem4  33109  nosupbnd2lem1  33113  slenlt  33129  madeval2  33188  brtxp  33239  brtxp2  33240  brpprod  33244  brpprod3a  33245  elfix  33262  dffix2  33264  ellimits  33269  sscoid  33272  dffun10  33273  elfuns  33274  elsingles  33277  brimg  33296  brapply  33297  brsuccf  33300  funpartlem  33301  brrestrict  33308  dfrecs2  33309  dfrdg4  33310  brlb  33314  altopthc  33330  altopthd  33331  fvtransport  33391  hfext  33542  nn0prpw  33569  filnetlem4  33627  df3nandALT2  33646  bj-sbeq  34116  bj-csbsnlem  34118  bj-elsngl  34178  bj-eltag  34187  bj-tagex  34197  bj-projun  34204  bj-reabeq  34237  bj-disj2r  34238  bj-restuni  34283  bj-elid6  34355  bj-eldiag  34361  bj-eldiag2  34362  topdifinffinlem  34511  relowlpssretop  34528  fvineqsneq  34576  wl-dfclab  34710  wl-dfrexsb  34733  phpreu  34758  poimirlem24  34798  poimirlem26  34800  poimirlem30  34804  areacirclem5  34868  isbnd2  34944  sbcalf  35275  sbcexf  35276  sbccom2  35286  sbccom2f  35287  sbccom2fi  35288  csbcom2fi  35289  anan  35382  idinxpssinxp2  35458  ineleq  35491  brabidga  35500  inxpxrn  35525  rnxrn  35528  cossssid2  35590  cossssid3  35591  cosscnvssid3  35598  dfeldisj3  35834  dfeldisj4  35835  prtlem70  35875  prtlem16  35887  ishlat2  36371  pmapglb  36788  polval2N  36924  dicelval3  38198  mapdordlem1a  38652  prjspeclsp  39142  fz1eqin  39246  7rexfrabdioph  39277  rmydioph  39491  dford4  39506  areaquad  39703  ifpan23  39705  ifpdfnan  39732  ifpdfxor  39733  ifpidg  39737  ifpid1g  39740  ifpim123g  39746  ifp1bi  39748  ifpimimb  39750  ifpororb  39751  ifpbibib  39756  rp-fakeuninass  39762  dfsucon  39769  cllem0  39805  rababg  39813  elmapintrab  39816  elmapintab  39836  undmrnresiss  39844  ss2iundf  39884  dfxor4  39991  rp-imass  39997  dfhe3  40001  dffrege115  40204  frege131  40220  frege133  40222  clsk1indlem4  40274  clsk1indlem1  40275  expandrexn  40507  rr-groth  40515  undisjrab  40518  pm13.196a  40626  eelT11  40921  eelTT1  40924  eelT01  40925  eel0T1  40926  uunTT1  41007  uunTT1p1  41008  uunTT1p2  41009  uunT11  41010  uunT11p1  41011  uunT11p2  41012  uun111  41019  iunssf  41232  ssrabf  41262  rabssf  41266  disjinfi  41334  elicores  41689  fourierdlem42  42315  iundjiun  42623  2reu7  43191  2reu8  43192  2reu8i  43193  dfdfat2  43208  aovov0bi  43276  afv2orxorb  43308  afv2ndeffv0  43340  ichcircshi  43459  icheq  43467  ichal  43474  prpair  43510  prproropf1olem0  43511  257prm  43570  fmtno4prmfac  43581  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  uspgrsprf1  43869  smndex1basss  43975  smndex1mgm  43977  opeliun2xp  44279  rrx2xpref1o  44603  aacllem  44800
  Copyright terms: Public domain W3C validator