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  432  anbi2ci  435  anbi12i  436  anbi12ci  437  pm5.3  447  an42  508  xchbinx  594  mt2bi  596  orbi12i  668  or42  676  pm5.53  702  orddi  721  anddi  722  pm2.1dc  733  notnot2dc  739  dcim  772  testbitestn  811  rbaib  818  rbaibr  819  pm4.43  842  orbididc  846  pm5.75  855  3orass  874  3anass  875  3ancomb  879  3anan32  882  3anan12  883  anandi3  884  anandi3r  885  xordc  1264  falbitru  1289  19.26-2  1347  19.26-3an  1348  alrot3  1350  alrot4OLD  1352  albiim  1353  2albiim  1354  19.27h  1430  19.27  1431  19.28h  1432  19.28  1433  nfalt  1448  aaanh  1456  aaan  1457  alinexa  1472  19.21-2  1535  nf2  1536  19.44  1550  19.45  1551  exrot3  1558  exrot4  1559  eeor  1563  sbcof2  1669  sbid2h  1707  19.23vv  1742  sbnv  1746  sblimv  1752  pm11.53  1753  19.41vv  1761  19.41vvv  1762  19.41vvvv  1763  19.42vv  1766  19.42vvv  1767  19.42vvvv  1768  4exdistr  1771  cbvex4v  1783  eean  1784  sbn  1804  sbim  1805  sbor  1806  sban  1807  sbrim  1808  sblim  1809  sbbi  1811  sblbis  1812  sbrbis  1813  sbrbif  1814  sbco2d  1818  sbco2vd  1819  sbnf2  1835  2sb5  1837  2sb6  1838  sbcom2v  1839  sbcom2v2  1840  sbcom2  1841  sb6a  1842  2sb5rf  1843  2sb6rf  1844  sbalyz  1853  sbal  1854  sbal1yz  1855  sbex  1858  sbalv  1859  sbco4lem  1860  exsb  1862  2exsb  1863  eujust  1880  euf  1883  cbveu  1902  mor  1920  eu2  1922  mo4f  1938  eu4  1940  2exeu  1970  2eu4  1971  exists1  1974  abid  2006  eleq12i  2083  abeq2  2124  abeq2i  2126  clabel  2141  abid2f  2180  sbabel  2181  neeq12i  2197  neanior  2266  ralnex  2290  ralinexa  2325  nfraldya  2332  nfrexdya  2333  r3al  2340  r19.26-2  2416  ralbiim  2421  r19.43  2442  ralcomf  2445  rexcomf  2446  rexrot4  2450  reean  2452  3reeanv  2454  rabbi  2461  cbvralf  2501  cbvrexf  2502  cbvreu  2505  cbvral2v  2515  cbvrex2v  2516  cbvral3v  2517  cbvralsv  2518  cbvrexsv  2519  sbralie  2520  rabeq2i  2528  issetf  2536  2gencl  2560  3gencl  2561  ceqsex2  2567  ceqsex3v  2569  ceqsex6v  2571  ceqsex8v  2572  gencbvex  2573  gencbval  2575  spc2gv  2616  eqvincf  2642  ceqsrex2v  2649  elrab2  2673  ralab  2674  ralrab  2675  rexab  2676  rexrab  2677  ralab2  2678  rexab2  2680  eueq3dc  2688  morex  2698  euind  2701  reu2  2702  reu6  2703  rmo4  2707  reu4  2708  reu7  2709  rmoim  2713  2reuswapdc  2716  reuind  2717  2rmorex  2718  sbcco  2758  sbccomlem  2805  sbccom  2806  ra5  2819  rmo3  2822  csbco  2834  sbnfc2  2879  csbabg  2880  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  dfss  2905  dfss2f  2909  ss2ab  2981  dfpss2  3002  dfpss3  3003  psseq12i  3008  difeqri  3037  raldifb  3056  uneqri  3058  ssequn2  3089  unss  3090  rexun  3096  ralunb  3097  elin2  3100  ineqri  3103  dfss1  3114  dfss5  3115  nsspssun  3143  ssddif  3144  difin  3147  indif  3153  difundi  3162  indifdir  3166  symdifxor  3176  inrab2  3183  rabun2  3189  reuun2  3193  0el  3214  rabeq0  3220  abeq0  3221  0pss  3238  disjr  3242  disj1  3243  disj4im  3249  disjpss  3251  undif4  3257  uneqdifeqim  3281  r19.3rmOLD  3283  r19.3rm  3285  r19.9rmv  3287  raaan  3302  pwss  3345  dfpr2  3362  ralsns  3378  rexsnsOLD  3380  eltpg  3386  ralprg  3391  rexprg  3392  raltpg  3393  rextpg  3394  snprc  3405  rabrsndc  3408  euabsn2  3409  eusn  3414  eldifsn  3465  rexdifsn  3469  eqsnm  3496  tpss  3499  snsssn  3502  prel12  3512  preqsn  3516  oprcl  3543  pwtpss  3547  eluniab  3562  elunirab  3563  unipr  3564  dfnfc2  3568  uniun  3569  uniin  3570  uni0b  3575  unissb  3580  elintab  3596  elintrab  3597  ssintab  3602  ssintrab  3608  intun  3616  intpr  3617  elrint  3625  iuncom4  3634  iuneq2  3643  dfiun2g  3659  ssiinf  3676  iundif2ss  3692  elriin  3697  iunxiun  3706  pwssb  3710  iunpwss  3713  dfdisj2  3717  cbvopab1  3800  dftr5  3827  trint  3839  inex1  3861  inuni  3879  repizf2lem  3884  unidif0  3890  axpweq  3894  bnd2  3896  zfpair2  3915  exss  3933  elop  3938  opm  3941  otth  3949  copsex4g  3954  opeqsn  3959  opelopabsbALT  3966  brabga  3971  opelopabaf  3980  iunopab  3988  pwunss  3990  pocl  4010  elsuci  4085  elsucg  4086  sucel  4092  unisucg  4096  uniuni  4129  reusv3  4138  iunpw  4157  setindel  4201  elirr  4204  en2lp  4212  ordpwsucss  4223  tfi  4228  peano2  4241  peano5  4244  elxp  4285  opelxp  4297  brxp  4298  rabxp  4303  opthprc  4314  brab2a  4316  opeliunxp  4318  xpundi  4319  xpundir  4320  elvvv  4326  brinxp  4331  brab2ga  4338  0xp  4343  ssrel2  4353  eqrelrel  4364  reliun  4381  reluni  4383  raliunxp  4400  rexiunxp  4401  ralxpf  4405  rexxpf  4406  iunxpf  4407  relop  4409  elcnv  4435  elcnv2  4436  dmin  4466  dmuni  4468  dmopab  4469  dmi  4473  dmmrnm  4477  rnopab  4504  elrnmpt1  4508  rncoeq  4528  resiexg  4576  dfima2  4593  dfima3  4594  elima2  4597  elima3  4598  imai  4604  elimasn  4615  epini  4619  dfse2  4621  cotr  4629  issref  4630  intasym  4632  asymref  4633  cnvopab  4649  cnvi  4651  cnvdif  4653  imainss  4662  rnxpid  4678  dfrel2  4694  dfrel3  4701  dmsnm  4709  rnsnm  4710  relsn2m  4714  dmsnopg  4715  cnvcnvsn  4720  elxp4  4731  elxp5  4732  cnvresima  4733  mptpreima  4737  dfco2  4743  coundi  4745  coundir  4746  imaco  4749  coiun  4753  coi1  4759  relssdmrn  4764  relrelss  4767  unixpm  4776  ressn  4781  cnviinm  4782  cnvpom  4783  cnvsom  4784  cbviota  4795  iotass  4807  dffun2  4835  dffun4  4836  dffun7  4850  dffun8  4851  dffun9  4852  funopab  4857  funun  4866  funcnvsn  4867  fntpg  4877  funcnv2  4881  funcnv  4882  fun2cnv  4885  fncnv  4887  fun11  4888  fununi  4889  imadiflem  4900  imadif  4901  imainlem  4902  funimaexglem  4904  fnunsn  4928  fnres  4937  fnopabg  4944  mptfng  4946  mptun  4951  fun  4984  fcnvres  4994  dff12  5012  f1cnvcnv  5021  funforn  5034  dff1o2  5052  dff1o5  5056  f1orn  5057  resdif  5069  ffoss  5079  f11o  5080  f1o00  5082  fo00  5083  elfv  5097  fv3  5118  nfvres  5127  eqfnfv3  5188  fneqeql  5196  unpreima  5213  respreima  5216  dffo3  5235  dffo5  5237  f1ompt  5241  ffnfvf  5245  fmptco  5251  ftpg  5268  fnressn  5270  idref  5317  abrexco  5319  dff13  5328  dff13f  5330  fliftel  5354  isoini  5378  eusvobj2  5418  acexmidlema  5423  acexmidlemb  5424  acexmidlemph  5425  acexmidlem2  5429  oprabid  5457  brabvv  5470  dfoprab2  5471  eqoprab2b  5482  dmoprab  5504  rnoprab  5506  eloprabga  5510  mpt2mptx  5514  resoprab  5516  ffnov  5524  elrnmpt2  5533  ralrnmpt2  5534  rexrnmpt2  5535  ovid  5536  ovi3  5556  ov6g  5557  foov  5566  opabex3d  5667  opabex3  5668  abexssex  5671  oprabex3  5675  oprabrexex2  5676  fmpt2  5746  xporderlem  5770  mpt2xopovel  5774  brtpos2  5784  dmtpos  5789  tpostpos  5797  tpossym  5809  tposoprab  5813  dfsmo2  5820  tfrlem7  5851  tfrlem9  5853  frecabex  5895  el1o  5931  dif1o  5932  dfer2  6014  brdifun  6040  eqerlem  6044  qsid  6078  iinerm  6085  riinerm  6086  erinxp  6087  brecop  6103  eroveu  6104  erovlem  6105  ecopovsym  6109  elni  6162  ltexpi  6191  enq0enq  6280  enq0ref  6282  enq0tr  6283  prarloclem3  6345  ltdfpr  6354  genpdflem  6355  genpassl  6373  genpassu  6374  nqprrnd  6392  ltexprlemopl  6432  ltexprlemopu  6434  ltexprlemdisj  6437  ltexprlemloc  6438  recexprlemdisj  6458  opelcn  6533  elreal  6535  elreal2  6536  axicn  6553  axprecex  6568  axpre-ltirr  6570  axpre-mulgt0  6574  xrlenlt  6679  ltxrlt  6680  bdcuni  7242  bdcriota  7249  bdinex1  7261  bj-zfpair2  7272  bj-axun2  7277  bj-ssom  7297
  Copyright terms: Public domain W3C validator