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

Theorem bitri 173
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 113 . . 3 (φψ)
3 bitri.2 . . 3 (ψχ)
42, 3sylib 127 . 2 (φχ)
53biimpri 124 . . 3 (χψ)
65, 1sylibr 137 . 2 (χφ)
74, 6impbii 117 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bitr2i  174  bitr3i  175  bitr4i  176  bitrd  177  3bitri  195  3bitr2i  197  3bitr3i  199  3bitr4i  201  bibi12i  218  imbi12i  228  pm4.71r  370  biadan2  429  anbi2ci  432  anbi12i  433  anbi12ci  434  pm5.3  444  an42  521  xchbinx  606  mt2bi  608  orbi12i  680  or42  688  pm5.53  714  orddi  732  anddi  733  pm2.1dc  744  notnot2dc  750  dcim  783  testbitestn  822  rbaib  829  rbaibr  830  pm4.43  855  orbididc  859  pm5.75  868  3orass  887  3anass  888  3ancomb  892  3anan32  895  3anan12  896  anandi3  897  anandi3r  898  xordc  1280  falbitru  1305  19.26-2  1368  19.26-3an  1369  alrot3  1371  albiim  1373  2albiim  1374  19.27h  1449  19.27  1450  19.28h  1451  19.28  1452  nfalt  1467  aaanh  1475  aaan  1476  alinexa  1491  19.21-2  1554  nf2  1555  19.44  1569  19.45  1570  exrot3  1577  exrot4  1578  eeor  1582  sbcof2  1688  sbid2h  1726  19.23vv  1761  sbnv  1765  sblimv  1771  pm11.53  1772  19.41vv  1780  19.41vvv  1781  19.41vvvv  1782  19.42vv  1785  19.42vvv  1786  19.42vvvv  1787  4exdistr  1790  cbvex4v  1802  eean  1803  sbn  1823  sbim  1824  sbor  1825  sban  1826  sbrim  1827  sblim  1828  sbbi  1830  sblbis  1831  sbrbis  1832  sbrbif  1833  sbco2d  1837  sbco2vd  1838  sbnf2  1854  2sb5  1856  2sb6  1857  sbcom2v  1858  sbcom2v2  1859  sbcom2  1860  sb6a  1861  2sb5rf  1862  2sb6rf  1863  sbalyz  1872  sbal  1873  sbal1yz  1874  sbex  1877  sbalv  1878  sbco4lem  1879  exsb  1881  2exsb  1882  eujust  1899  euf  1902  cbveu  1921  mor  1939  eu2  1941  mo4f  1957  eu4  1959  2exeu  1989  2eu4  1990  exists1  1993  abid  2025  eleq12i  2102  abeq2  2143  abeq2i  2145  clabel  2160  abid2f  2199  sbabel  2200  neeq12i  2217  neanior  2286  ralnex  2310  ralinexa  2345  nfraldya  2352  nfrexdya  2353  r3al  2360  r19.26-2  2436  ralbiim  2441  r19.43  2462  ralcomf  2465  rexcomf  2466  rexrot4  2470  reean  2472  3reeanv  2474  rabbi  2481  cbvralf  2521  cbvrexf  2522  cbvreu  2525  cbvral2v  2535  cbvrex2v  2536  cbvral3v  2537  cbvralsv  2538  cbvrexsv  2539  sbralie  2540  rabeq2i  2548  issetf  2556  2gencl  2581  3gencl  2582  ceqsex2  2588  ceqsex3v  2590  ceqsex6v  2592  ceqsex8v  2593  gencbvex  2594  gencbval  2596  spc2gv  2637  eqvincf  2663  ceqsrex2v  2670  elrab2  2694  ralab  2695  ralrab  2696  rexab  2697  rexrab  2698  ralab2  2699  rexab2  2701  eueq3dc  2709  morex  2719  euind  2722  reu2  2723  reu6  2724  rmo4  2728  reu4  2729  reu7  2730  rmoim  2734  2reuswapdc  2737  reuind  2738  2rmorex  2739  sbcco  2779  sbccomlem  2826  sbccom  2827  ra5  2840  rmo3  2843  csbco  2855  sbnfc2  2900  csbabg  2901  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  dfss  2926  dfss2f  2930  ss2ab  3002  dfpss2  3023  dfpss3  3024  psseq12i  3029  difeqri  3058  raldifb  3077  uneqri  3079  ssequn2  3110  unss  3111  rexun  3117  ralunb  3118  elin2  3121  ineqri  3124  dfss1  3135  dfss5  3136  nsspssun  3164  ssddif  3165  difin  3168  indif  3174  difundi  3183  indifdir  3187  symdifxor  3197  inrab2  3204  rabun2  3210  reuun2  3214  0el  3235  rabeq0  3241  abeq0  3242  0pss  3259  disjr  3263  disj1  3264  disj4im  3270  disjpss  3272  undif4  3278  uneqdifeqim  3302  r19.3rm  3304  r19.9rmv  3307  raaan  3321  pwss  3366  dfpr2  3383  ralsns  3399  rexsnsOLD  3401  eltpg  3407  ralprg  3412  rexprg  3413  raltpg  3414  rextpg  3415  snprc  3426  rabrsndc  3429  euabsn2  3430  eusn  3435  eldifsn  3486  rexdifsn  3490  eqsnm  3517  tpss  3520  snsssn  3523  prel12  3533  preqsn  3537  oprcl  3564  pwtpss  3568  eluniab  3583  elunirab  3584  unipr  3585  dfnfc2  3589  uniun  3590  uniin  3591  uni0b  3596  unissb  3601  elintab  3617  elintrab  3618  ssintab  3623  ssintrab  3629  intun  3637  intpr  3638  elrint  3646  iuncom4  3655  iuneq2  3664  dfiun2g  3680  ssiinf  3697  iundif2ss  3713  elriin  3718  iunxiun  3727  pwssb  3731  iunpwss  3734  dfdisj2  3738  cbvopab1  3821  dftr5  3848  trint  3860  inex1  3882  inuni  3900  repizf2lem  3905  unidif0  3911  axpweq  3915  bnd2  3917  zfpair2  3936  exss  3954  elop  3959  opm  3962  otth  3970  copsex4g  3975  opeqsn  3980  opelopabsbALT  3987  brabga  3992  opelopabaf  4001  iunopab  4009  pwunss  4011  pocl  4031  elsuci  4106  elsucg  4107  sucel  4113  unisucg  4117  uniuni  4149  reusv3  4158  iunpw  4177  setindel  4221  elirr  4224  en2lp  4232  ordpwsucss  4243  tfi  4248  peano2  4261  peano5  4264  elxp  4305  opelxp  4317  brxp  4318  rabxp  4323  opthprc  4334  brab2a  4336  opeliunxp  4338  xpundi  4339  xpundir  4340  elvvv  4346  brinxp  4351  brab2ga  4358  0xp  4363  ssrel2  4373  eqrelrel  4384  reliun  4401  reluni  4403  raliunxp  4420  rexiunxp  4421  ralxpf  4425  rexxpf  4426  iunxpf  4427  relop  4429  elcnv  4455  elcnv2  4456  dmin  4486  dmuni  4488  dmopab  4489  dmi  4493  dmmrnm  4497  rnopab  4524  elrnmpt1  4528  rncoeq  4548  resiexg  4596  dfima2  4613  dfima3  4614  elima2  4617  elima3  4618  imai  4624  elimasn  4635  epini  4639  dfse2  4641  cotr  4649  issref  4650  intasym  4652  asymref  4653  cnvopab  4669  cnvi  4671  cnvdif  4673  imainss  4682  rnxpid  4698  dfrel2  4714  dfrel3  4721  dmsnm  4729  rnsnm  4730  relsn2m  4734  dmsnopg  4735  cnvcnvsn  4740  elxp4  4751  elxp5  4752  cnvresima  4753  mptpreima  4757  dfco2  4763  coundi  4765  coundir  4766  imaco  4769  coiun  4773  coi1  4779  relssdmrn  4784  relrelss  4787  unixpm  4796  ressn  4801  cnviinm  4802  cnvpom  4803  cnvsom  4804  cbviota  4815  iotass  4827  dffun2  4855  dffun4  4856  dffun7  4871  dffun8  4872  dffun9  4873  funopab  4878  funun  4887  funcnvsn  4888  fntpg  4898  funcnv2  4902  funcnv  4903  fun2cnv  4906  fncnv  4908  fun11  4909  fununi  4910  imadiflem  4921  imadif  4922  imainlem  4923  funimaexglem  4925  fnunsn  4949  fnres  4958  fnopabg  4965  mptfng  4967  mptun  4972  fun  5006  fcnvres  5016  dff12  5034  f1cnvcnv  5043  funforn  5056  dff1o2  5074  dff1o5  5078  f1orn  5079  resdif  5091  ffoss  5101  f11o  5102  f1o00  5104  fo00  5105  elfv  5119  fv3  5140  nfvres  5149  eqfnfv3  5210  fneqeql  5218  unpreima  5235  respreima  5238  dffo3  5257  dffo5  5259  f1ompt  5263  ffnfvf  5267  fmptco  5273  ftpg  5290  fnressn  5292  idref  5339  abrexco  5341  dff13  5350  dff13f  5352  fliftel  5376  isoini  5400  eusvobj2  5441  acexmidlema  5446  acexmidlemb  5447  acexmidlemph  5448  acexmidlem2  5452  oprabid  5480  brabvv  5493  dfoprab2  5494  eqoprab2b  5505  dmoprab  5527  rnoprab  5529  eloprabga  5533  mpt2mptx  5537  resoprab  5539  ffnov  5547  elrnmpt2  5556  ralrnmpt2  5557  rexrnmpt2  5558  ovid  5559  ovi3  5579  ov6g  5580  foov  5589  opabex3d  5690  opabex3  5691  abexssex  5694  oprabex3  5698  oprabrexex2  5699  fmpt2  5769  xporderlem  5793  mpt2xopovel  5797  brtpos2  5807  dmtpos  5812  tpostpos  5820  tpossym  5832  tposoprab  5836  dfsmo2  5843  tfrlem7  5874  tfrlem9  5876  frecabex  5923  el1o  5959  dif1o  5960  dfer2  6043  brdifun  6069  eqerlem  6073  qsid  6107  iinerm  6114  riinerm  6115  erinxp  6116  brecop  6132  eroveu  6133  erovlem  6134  ecopovsym  6138  domen  6168  isfi  6177  en1  6215  xpsnen  6231  xpcomco  6236  xpassen  6240  elni  6292  ltexpi  6321  enq0enq  6413  enq0ref  6415  enq0tr  6416  prarloclem3  6479  ltdfpr  6488  genpdflem  6489  genpassl  6507  genpassu  6508  nqprrnd  6526  ltexprlemopl  6573  ltexprlemopu  6575  ltexprlemdisj  6578  ltexprlemloc  6579  recexprlemdisj  6600  opelcn  6685  elreal  6687  elreal2  6688  axicn  6709  axprecex  6724  axpre-ltirr  6726  axpre-mulgt0  6731  xrlenlt  6841  ltxrlt  6842  inelr  7328  reapcotr  7342  1nn  7666  elnnne0  7931  un0addcl  7951  un0mulcl  7952  elnnz  7991  elznn0nn  7995  elznn0  7996  elznn  7997  elz2  8048  zapne  8051  prime  8073  raluz2  8258  rexuz2  8260  eluz2b2  8276  eluz2b3  8277  ublbneg  8284  elq  8293  qreccl  8311  ralrp  8339  rexrp  8340  rpnegap  8350  ltxr  8425  xrnemnf  8429  xrltso  8447  icc0r  8525  divelunit  8600  fzprval  8674  fztpval  8675  elfz1b  8682  4fvwrd4  8727  fzolb  8739  fzolb2  8740  elfzo3  8749  fzouzsplit  8765  elfzo0z  8770  fzo0m  8777  fzind2  8825  bdcuni  9265  bdcriota  9272  bdinex1  9284  bj-zfpair2  9295  bj-axun2  9300  bj-ssom  9324
  Copyright terms: Public domain W3C validator