ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bitri GIF version

Theorem bitri 182
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypotheses
Ref Expression
bitri.1 (𝜑𝜓)
bitri.2 (𝜓𝜒)
Assertion
Ref Expression
bitri (𝜑𝜒)

Proof of Theorem bitri
StepHypRef Expression
1 bitri.1 . . . 4 (𝜑𝜓)
21biimpi 118 . . 3 (𝜑𝜓)
3 bitri.2 . . 3 (𝜓𝜒)
42, 3sylib 120 . 2 (𝜑𝜒)
53biimpri 131 . . 3 (𝜒𝜓)
65, 1sylibr 132 . 2 (𝜒𝜑)
74, 6impbii 124 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bitr2i  183  bitr3i  184  bitr4i  185  bitrd  186  3bitri  204  3bitr2i  206  3bitr3i  208  3bitr4i  210  bibi12i  227  imbi12i  237  pm4.71r  382  biadan2  444  anbi2ci  447  anbi12i  448  anbi12ci  449  pm5.3  459  an42  552  xchbinx  640  mt2bi  642  orbi12i  714  or42  722  pm5.53  749  orddi  767  anddi  768  pm2.1dc  781  notnotrdc  787  dcim  820  testbitestn  859  rbaib  866  rbaibr  867  pm4.43  893  orbididc  897  pm5.75  906  3orass  925  3anass  926  3ancomb  930  3anan32  933  3anan12  934  anandi3  935  anandi3r  936  xordc  1326  falbitru  1351  19.26-2  1414  19.26-3an  1415  alrot3  1417  albiim  1419  2albiim  1420  19.27h  1495  19.27  1496  19.28h  1497  19.28  1498  nfalt  1513  aaanh  1521  aaan  1522  alinexa  1537  19.21-2  1600  nf2  1601  19.44  1615  19.45  1616  exrot3  1623  exrot4  1624  eeor  1628  sbcof2  1735  sbid2h  1774  19.23vv  1809  sbnv  1813  sblimv  1819  pm11.53  1820  19.41vv  1828  19.41vvv  1829  19.41vvvv  1830  19.42vv  1833  19.42vvv  1834  19.42vvvv  1835  4exdistr  1838  cbvex4v  1850  eean  1851  sbn  1871  sbim  1872  sbor  1873  sban  1874  sbrim  1875  sblim  1876  sbbi  1878  sblbis  1879  sbrbis  1880  sbrbif  1881  sbco2d  1885  sbco2vd  1886  sbnf2  1902  2sb5  1904  2sb6  1905  sbcom2v  1906  sbcom2v2  1907  sbcom2  1908  sb6a  1909  2sb5rf  1910  2sb6rf  1911  sbalyz  1920  sbal  1921  sbal1yz  1922  sbex  1925  sbalv  1926  sbco4lem  1927  exsb  1929  2exsb  1930  eujust  1947  euf  1950  cbveu  1969  mor  1987  eu2  1989  mo4f  2005  eu4  2007  2exeu  2037  2eu4  2038  exists1  2041  abid  2073  eleq12i  2152  abeq2  2193  abeq2i  2195  clabel  2210  abid2f  2249  sbabel  2250  neeq12i  2268  neanior  2338  ralnex  2365  dfrex2dc  2367  ralinexa  2401  nfraldya  2408  nfrexdya  2409  r3al  2416  r19.26-2  2494  ralbiim  2499  r19.43  2521  ralcomf  2524  rexcomf  2525  rexrot4  2529  reean  2531  3reeanv  2533  rabbi  2540  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvral2v  2594  cbvrex2v  2595  cbvral3v  2596  cbvralsv  2597  cbvrexsv  2598  sbralie  2599  rabeq2i  2612  issetf  2620  2gencl  2646  3gencl  2647  ceqsex2  2653  ceqsex3v  2655  ceqsex6v  2657  ceqsex8v  2658  gencbvex  2659  gencbval  2661  spc2gv  2702  eqvincf  2733  ceqsrex2v  2740  elrab2  2765  ralab  2766  ralrab  2767  rexab  2768  rexrab  2769  ralab2  2770  rexab2  2772  eueq3dc  2780  morex  2790  euind  2793  reu2  2794  reu6  2795  rmo4  2799  reu4  2800  reu7  2801  rmoim  2805  2reuswapdc  2808  reuind  2809  2rmorex  2810  sbcco  2850  sbccomlem  2902  sbccom  2903  ra5  2916  rmo3  2919  csbco  2931  sbnfc2  2977  csbabg  2978  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  dfss  3002  dfss2f  3005  ss2ab  3078  dfdif3  3099  difeqri  3109  ddifstab  3121  raldifb  3129  uneqri  3131  ssequn2  3162  unss  3163  rexun  3169  ralunb  3170  elin2  3177  ineqri  3182  dfss1  3193  dfss5  3194  dfss4st  3221  ssddif  3222  difin  3225  indif  3231  difundi  3240  indifdir  3244  symdifxor  3254  inrab2  3261  rabun2  3267  reuun2  3271  0el  3294  rabeq0  3301  abeq0  3302  disjr  3320  disj1  3321  undif4  3333  uneqdifeqim  3355  r19.3rm  3357  r19.9rmv  3360  raaan  3375  pwss  3430  dfpr2  3450  ralsnsg  3465  ralsns  3466  eltpg  3473  ralprg  3478  rexprg  3479  raltpg  3480  rextpg  3481  snprc  3492  rabrsndc  3495  euabsn2  3496  eusn  3501  eldifsn  3552  ssdifsn  3553  rexdifsn  3557  eqsnm  3584  tpss  3587  snsssn  3590  prel12  3600  preqsn  3604  oprcl  3631  pwtpss  3635  eluniab  3650  elunirab  3651  unipr  3652  dfnfc2  3656  uniun  3657  uniin  3658  uni0b  3663  unissb  3668  elintab  3684  elintrab  3685  ssintab  3690  ssintrab  3696  intun  3704  intpr  3705  elrint  3713  iuncom4  3722  iuneq2  3731  dfiun2g  3747  ssiinf  3764  iundif2ss  3780  elriin  3785  iunxiun  3794  pwssb  3798  iunpwss  3801  dfdisj2  3805  cbvopab1  3888  dftr5  3916  trint  3928  inex1  3950  inuni  3968  repizf2lem  3973  unidif0  3979  axpweq  3983  bnd2  3985  exmid01  4008  zfpair2  4013  exss  4030  elop  4034  opm  4037  otth  4045  copsex4g  4050  opeqsn  4055  opelopabsbALT  4062  brabga  4067  opelopabaf  4076  iunopab  4084  pwunss  4086  pocl  4106  frirrg  4153  elsuci  4206  elsucg  4207  sucel  4213  unisucg  4217  uniuni  4249  reusv3  4258  iunpw  4277  setindel  4329  elirr  4332  en2lp  4345  ordpwsucss  4358  zfregfr  4364  tfi  4372  peano2  4385  peano5  4388  elxp  4430  opelxp  4442  brxp  4443  rabxp  4448  opthprc  4459  brab2a  4461  opeliunxp  4463  xpundi  4464  xpundir  4465  elvvv  4471  brinxp  4476  brab2ga  4483  0xp  4488  ssrel2  4498  eqrelrel  4509  reliun  4528  reluni  4530  raliunxp  4547  rexiunxp  4548  ralxpf  4552  rexxpf  4553  iunxpf  4554  relop  4556  elco  4572  elcnv  4583  elcnv2  4584  dmin  4614  dmuni  4616  dmopab  4617  dmi  4621  dmmrnm  4625  rnopab  4652  elrnmpt1  4656  rncoeq  4676  resiexg  4726  dfima2  4745  dfima3  4746  elima2  4749  elima3  4750  imai  4757  elimasn  4768  epini  4772  dfse2  4774  cotr  4782  issref  4783  intasym  4785  asymref  4786  cnvopab  4802  cnvi  4804  cnvdif  4806  imainss  4815  rnxpid  4833  dfrel2  4849  dfrel3  4856  dmsnm  4864  rnsnm  4865  relsn2m  4869  dmsnopg  4870  cnvcnvsn  4875  elxp4  4886  elxp5  4887  cnvresima  4888  mptpreima  4892  dfco2  4898  coundi  4900  coundir  4901  imaco  4904  coiun  4908  coi1  4914  relssdmrn  4919  relrelss  4925  unixpm  4934  ressn  4939  cnviinm  4940  cnvpom  4941  cnvsom  4942  cbviota  4953  iotass  4965  dffun2  4993  dffun4  4994  dffun7  5009  dffun8  5010  dffun9  5011  funopab  5016  funun  5025  funcnvsn  5026  fntpg  5037  funcnv2  5041  funcnv  5042  fun2cnv  5045  fncnv  5047  fun11  5048  fununi  5049  imadiflem  5060  imadif  5061  imainlem  5062  funimaexglem  5064  fnunsn  5088  fnres  5097  fnopabg  5104  mptfng  5106  mptun  5111  fun  5149  fcnvres  5159  dff12  5180  f1cnvcnv  5192  funforn  5205  dff1o2  5223  dff1o5  5227  f1orn  5228  resdif  5240  ffoss  5250  f11o  5251  f1o00  5253  fo00  5254  elfv  5268  fv3  5293  nfvres  5302  eqfnfv3  5364  fneqeql  5372  unpreima  5389  respreima  5392  dffo3  5411  dffo5  5413  f1ompt  5415  ffnfvf  5422  fmptco  5429  ftpg  5446  fnressn  5448  idref  5499  abrexco  5501  dff13  5510  dff13f  5512  fliftel  5535  isoini  5560  eusvobj2  5601  acexmidlema  5606  acexmidlemb  5607  acexmidlemph  5608  acexmidlem2  5612  oprabid  5640  brabvv  5654  dfoprab2  5655  eqoprab2b  5666  dmoprab  5688  rnoprab  5690  eloprabga  5694  mpt2mptx  5698  resoprab  5700  ffnov  5708  elrnmpt2  5717  ralrnmpt2  5718  rexrnmpt2  5719  ovid  5720  ovi3  5740  ov6g  5741  foov  5750  opabex3d  5851  opabex3  5852  abexssex  5855  oprabex3  5859  oprabrexex2  5860  fmpt2  5930  xporderlem  5955  f1od2  5959  mpt2xopovel  5962  brtpos2  5972  dmtpos  5977  tpostpos  5985  tpossym  5997  tposoprab  6001  dfsmo2  6008  tfrlem7  6038  tfrlem9  6040  tfr1onlemaccex  6069  tfrcllemaccex  6082  tfrcldm  6084  frecabex  6119  el1o  6157  dif1o  6158  dfer2  6247  brdifun  6273  eqerlem  6277  qsid  6311  iinerm  6318  riinerm  6319  erinxp  6320  brecop  6336  eroveu  6337  erovlem  6338  ecopovsym  6342  mapval2  6389  mapsn  6401  domen  6422  isfi  6432  en1  6470  xpsnen  6491  xpcomco  6496  xpassen  6500  ssenen  6521  nneneq  6527  snnen2oprc  6530  ac6sfi  6568  exmidpw  6578  eldju  6706  eldju2ndl  6710  eldju2ndr  6711  finomni  6743  elni  6814  ltexpi  6843  enq0enq  6937  enq0ref  6939  enq0tr  6940  prarloclem3  7003  ltdfpr  7012  genpdflem  7013  genpassl  7030  genpassu  7031  nqprrnd  7049  nqprl  7057  nqpru  7058  ltexprlemopl  7107  ltexprlemopu  7109  ltexprlemdisj  7112  ltexprlemloc  7113  recexprlemdisj  7136  caucvgprprlemell  7191  caucvgprprlemelu  7192  opelcn  7311  elreal  7313  elreal2  7315  peano1nnnn  7336  axicn  7347  axprecex  7362  axpre-ltirr  7364  axpre-mulgt0  7369  axcaucvglemres  7381  xrlenlt  7498  ltxrlt  7499  inelr  8005  reapcotr  8019  1nn  8371  elnnne0  8623  un0addcl  8642  un0mulcl  8643  elnnz  8696  elznn0nn  8700  elznn0  8701  elznn  8702  elz2  8754  zapne  8757  3halfnz  8779  prime  8781  raluz2  9002  rexuz2  9004  supinfneg  9018  infsupneg  9019  eluz2b2  9025  eluz2b3  9026  ublbneg  9033  elq  9042  qreccl  9062  ralrp  9090  rexrp  9091  rpnegap  9101  ltxr  9181  xrnemnf  9183  xrltso  9201  icc0r  9279  divelunit  9354  fzprval  9429  fztpval  9430  elfz1b  9437  fz01or  9458  4fvwrd4  9482  fzolb  9495  fzolb2  9496  elfzo3  9505  fzouzsplit  9521  elfzo0z  9526  fzo0m  9533  fzind2  9581  ioo0  9602  ico0  9604  ioc0  9605  iseqf1olemp  9839  caucvgre  10313  cvg1nlemcau  10316  resqrexlemex  10357  climeu  10582  divides  10704  m1exp1  10807  divalgb  10831  bezoutlemnewy  10891  bezoutlemmain  10893  bezoutlemex  10896  dfgcd2  10909  lcmgcdlem  10965  isprm2  11005  isprm3  11006  isprm4  11007  sqrt2irr  11047  oddpwdc  11058  decidr  11165  bdcuni  11236  bdcriota  11243  bdinex1  11259  bj-zfpair2  11270  bj-axun2  11275  bj-ssom  11300  ss1oel2o  11357  nninfsellemdc  11371  nninfsellemsuc  11373  nninfsellemqall  11376
  Copyright terms: Public domain W3C validator