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

Theorem bitri 177
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 117 . . 3 (𝜑𝜓)
3 bitri.2 . . 3 (𝜓𝜒)
42, 3sylib 131 . 2 (𝜑𝜒)
53biimpri 128 . . 3 (𝜒𝜓)
65, 1sylibr 141 . 2 (𝜒𝜑)
74, 6impbii 121 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  bitr2i  178  bitr3i  179  bitr4i  180  bitrd  181  3bitri  199  3bitr2i  201  3bitr3i  203  3bitr4i  205  bibi12i  222  imbi12i  232  pm4.71r  376  biadan2  437  anbi2ci  440  anbi12i  441  anbi12ci  442  pm5.3  452  an42  529  xchbinx  617  mt2bi  619  orbi12i  691  or42  699  pm5.53  726  orddi  744  anddi  745  pm2.1dc  756  notnotrdc  762  dcim  795  testbitestn  834  rbaib  841  rbaibr  842  pm4.43  867  orbididc  871  pm5.75  880  3orass  899  3anass  900  3ancomb  904  3anan32  907  3anan12  908  anandi3  909  anandi3r  910  xordc  1299  falbitru  1324  19.26-2  1387  19.26-3an  1388  alrot3  1390  albiim  1392  2albiim  1393  19.27h  1468  19.27  1469  19.28h  1470  19.28  1471  nfalt  1486  aaanh  1494  aaan  1495  alinexa  1510  19.21-2  1573  nf2  1574  19.44  1588  19.45  1589  exrot3  1596  exrot4  1597  eeor  1601  sbcof2  1707  sbid2h  1745  19.23vv  1780  sbnv  1784  sblimv  1790  pm11.53  1791  19.41vv  1799  19.41vvv  1800  19.41vvvv  1801  19.42vv  1804  19.42vvv  1805  19.42vvvv  1806  4exdistr  1809  cbvex4v  1821  eean  1822  sbn  1842  sbim  1843  sbor  1844  sban  1845  sbrim  1846  sblim  1847  sbbi  1849  sblbis  1850  sbrbis  1851  sbrbif  1852  sbco2d  1856  sbco2vd  1857  sbnf2  1873  2sb5  1875  2sb6  1876  sbcom2v  1877  sbcom2v2  1878  sbcom2  1879  sb6a  1880  2sb5rf  1881  2sb6rf  1882  sbalyz  1891  sbal  1892  sbal1yz  1893  sbex  1896  sbalv  1897  sbco4lem  1898  exsb  1900  2exsb  1901  eujust  1918  euf  1921  cbveu  1940  mor  1958  eu2  1960  mo4f  1976  eu4  1978  2exeu  2008  2eu4  2009  exists1  2012  abid  2044  eleq12i  2121  abeq2  2162  abeq2i  2164  clabel  2179  abid2f  2218  sbabel  2219  neeq12i  2237  neanior  2307  ralnex  2333  ralinexa  2368  nfraldya  2375  nfrexdya  2376  r3al  2383  r19.26-2  2459  ralbiim  2464  r19.43  2485  ralcomf  2488  rexcomf  2489  rexrot4  2493  reean  2495  3reeanv  2497  rabbi  2504  cbvralf  2544  cbvrexf  2545  cbvreu  2548  cbvral2v  2558  cbvrex2v  2559  cbvral3v  2560  cbvralsv  2561  cbvrexsv  2562  sbralie  2563  rabeq2i  2571  issetf  2579  2gencl  2604  3gencl  2605  ceqsex2  2611  ceqsex3v  2613  ceqsex6v  2615  ceqsex8v  2616  gencbvex  2617  gencbval  2619  spc2gv  2660  eqvincf  2692  ceqsrex2v  2699  elrab2  2723  ralab  2724  ralrab  2725  rexab  2726  rexrab  2727  ralab2  2728  rexab2  2730  eueq3dc  2738  morex  2748  euind  2751  reu2  2752  reu6  2753  rmo4  2757  reu4  2758  reu7  2759  rmoim  2763  2reuswapdc  2766  reuind  2767  2rmorex  2768  sbcco  2808  sbccomlem  2860  sbccom  2861  ra5  2874  rmo3  2877  csbco  2889  sbnfc2  2934  csbabg  2935  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  dfss  2960  dfss2f  2964  ss2ab  3036  dfpss2  3057  dfpss3  3058  psseq12i  3063  difeqri  3092  raldifb  3111  uneqri  3113  ssequn2  3144  unss  3145  rexun  3151  ralunb  3152  elin2  3155  ineqri  3158  dfss1  3169  dfss5  3170  nsspssun  3198  ssddif  3199  difin  3202  indif  3208  difundi  3217  indifdir  3221  symdifxor  3231  inrab2  3238  rabun2  3244  reuun2  3248  0el  3269  rabeq0  3275  abeq0  3276  0pss  3293  disjr  3297  disj1  3298  disj4im  3304  disjpss  3306  undif4  3312  uneqdifeqim  3336  r19.3rm  3338  r19.9rmv  3341  raaan  3355  pwss  3402  dfpr2  3422  ralsnsg  3435  ralsns  3436  rexsnsOLD  3438  eltpg  3444  ralprg  3449  rexprg  3450  raltpg  3451  rextpg  3452  snprc  3463  rabrsndc  3466  euabsn2  3467  eusn  3472  eldifsn  3523  rexdifsn  3527  eqsnm  3554  tpss  3557  snsssn  3560  prel12  3570  preqsn  3574  oprcl  3601  pwtpss  3605  eluniab  3620  elunirab  3621  unipr  3622  dfnfc2  3626  uniun  3627  uniin  3628  uni0b  3633  unissb  3638  elintab  3654  elintrab  3655  ssintab  3660  ssintrab  3666  intun  3674  intpr  3675  elrint  3683  iuncom4  3692  iuneq2  3701  dfiun2g  3717  ssiinf  3734  iundif2ss  3750  elriin  3755  iunxiun  3764  pwssb  3768  iunpwss  3771  dfdisj2  3775  cbvopab1  3858  dftr5  3885  trint  3897  inex1  3919  inuni  3937  repizf2lem  3942  unidif0  3948  axpweq  3952  bnd2  3954  zfpair2  3973  exss  3991  elop  3996  opm  3999  otth  4007  copsex4g  4012  opeqsn  4017  opelopabsbALT  4024  brabga  4029  opelopabaf  4038  iunopab  4046  pwunss  4048  pocl  4068  frirrg  4115  elsuci  4168  elsucg  4169  sucel  4175  unisucg  4179  uniuni  4211  reusv3  4220  iunpw  4239  setindel  4291  elirr  4294  en2lp  4306  ordpwsucss  4319  zfregfr  4326  tfi  4333  peano2  4346  peano5  4349  elxp  4390  opelxp  4402  brxp  4403  rabxp  4408  opthprc  4419  brab2a  4421  opeliunxp  4423  xpundi  4424  xpundir  4425  elvvv  4431  brinxp  4436  brab2ga  4443  0xp  4448  ssrel2  4458  eqrelrel  4469  reliun  4486  reluni  4488  raliunxp  4505  rexiunxp  4506  ralxpf  4510  rexxpf  4511  iunxpf  4512  relop  4514  elcnv  4540  elcnv2  4541  dmin  4571  dmuni  4573  dmopab  4574  dmi  4578  dmmrnm  4582  rnopab  4609  elrnmpt1  4613  rncoeq  4633  resiexg  4681  dfima2  4698  dfima3  4699  elima2  4702  elima3  4703  imai  4709  elimasn  4720  epini  4724  dfse2  4726  cotr  4734  issref  4735  intasym  4737  asymref  4738  cnvopab  4754  cnvi  4756  cnvdif  4758  imainss  4767  rnxpid  4783  dfrel2  4799  dfrel3  4806  dmsnm  4814  rnsnm  4815  relsn2m  4819  dmsnopg  4820  cnvcnvsn  4825  elxp4  4836  elxp5  4837  cnvresima  4838  mptpreima  4842  dfco2  4848  coundi  4850  coundir  4851  imaco  4854  coiun  4858  coi1  4864  relssdmrn  4869  relrelss  4872  unixpm  4881  ressn  4886  cnviinm  4887  cnvpom  4888  cnvsom  4889  cbviota  4900  iotass  4912  dffun2  4940  dffun4  4941  dffun7  4956  dffun8  4957  dffun9  4958  funopab  4963  funun  4972  funcnvsn  4973  fntpg  4983  funcnv2  4987  funcnv  4988  fun2cnv  4991  fncnv  4993  fun11  4994  fununi  4995  imadiflem  5006  imadif  5007  imainlem  5008  funimaexglem  5010  fnunsn  5034  fnres  5043  fnopabg  5050  mptfng  5052  mptun  5057  fun  5091  fcnvres  5101  dff12  5119  f1cnvcnv  5128  funforn  5141  dff1o2  5159  dff1o5  5163  f1orn  5164  resdif  5176  ffoss  5186  f11o  5187  f1o00  5189  fo00  5190  elfv  5204  fv3  5225  nfvres  5234  eqfnfv3  5295  fneqeql  5303  unpreima  5320  respreima  5323  dffo3  5342  dffo5  5344  f1ompt  5348  ffnfvf  5352  fmptco  5358  ftpg  5375  fnressn  5377  idref  5424  abrexco  5426  dff13  5435  dff13f  5437  fliftel  5461  isoini  5485  eusvobj2  5526  acexmidlema  5531  acexmidlemb  5532  acexmidlemph  5533  acexmidlem2  5537  oprabid  5565  brabvv  5579  dfoprab2  5580  eqoprab2b  5591  dmoprab  5613  rnoprab  5615  eloprabga  5619  mpt2mptx  5623  resoprab  5625  ffnov  5633  elrnmpt2  5642  ralrnmpt2  5643  rexrnmpt2  5644  ovid  5645  ovi3  5665  ov6g  5666  foov  5675  opabex3d  5776  opabex3  5777  abexssex  5780  oprabex3  5784  oprabrexex2  5785  fmpt2  5855  xporderlem  5880  f1od2  5884  mpt2xopovel  5887  brtpos2  5897  dmtpos  5902  tpostpos  5910  tpossym  5922  tposoprab  5926  dfsmo2  5933  tfrlem7  5964  tfrlem9  5966  frecabex  6015  el1o  6051  dif1o  6052  dfer2  6138  brdifun  6164  eqerlem  6168  qsid  6202  iinerm  6209  riinerm  6210  erinxp  6211  brecop  6227  eroveu  6228  erovlem  6229  ecopovsym  6233  domen  6263  isfi  6272  en1  6310  xpsnen  6326  xpcomco  6331  xpassen  6335  nneneq  6351  snnen2oprc  6354  ac6sfi  6383  elni  6464  ltexpi  6493  enq0enq  6587  enq0ref  6589  enq0tr  6590  prarloclem3  6653  ltdfpr  6662  genpdflem  6663  genpassl  6680  genpassu  6681  nqprrnd  6699  nqprl  6707  nqpru  6708  ltexprlemopl  6757  ltexprlemopu  6759  ltexprlemdisj  6762  ltexprlemloc  6763  recexprlemdisj  6786  caucvgprprlemell  6841  caucvgprprlemelu  6842  opelcn  6961  elreal  6963  elreal2  6965  peano1nnnn  6986  axicn  6997  axprecex  7012  axpre-ltirr  7014  axpre-mulgt0  7019  axcaucvglemres  7031  xrlenlt  7143  ltxrlt  7144  inelr  7649  reapcotr  7663  1nn  8001  elnnne0  8253  un0addcl  8272  un0mulcl  8273  elnnz  8312  elznn0nn  8316  elznn0  8317  elznn  8318  elz2  8370  zapne  8373  3halfnz  8395  prime  8396  raluz2  8618  rexuz2  8620  eluz2b2  8637  eluz2b3  8638  ublbneg  8645  elq  8654  qreccl  8674  ralrp  8702  rexrp  8703  rpnegap  8713  ltxr  8796  xrnemnf  8800  xrltso  8818  icc0r  8896  divelunit  8971  fzprval  9046  fztpval  9047  elfz1b  9054  4fvwrd4  9099  fzolb  9111  fzolb2  9112  elfzo3  9121  fzouzsplit  9137  elfzo0z  9142  fzo0m  9149  fzind2  9197  ioo0  9216  ico0  9218  ioc0  9219  caucvgre  9808  cvg1nlemcau  9811  resqrexlemex  9852  climeu  10048  divides  10110  fz01or  10190  m1exp1  10213  divalgb  10237  sqrt2irr  10251  oddpwdc  10262  bdcuni  10383  bdcriota  10390  bdinex1  10406  bj-zfpair2  10417  bj-axun2  10422  bj-ssom  10447
  Copyright terms: Public domain W3C validator