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

Theorem bitri 183
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  |-  ( ph  <->  ps )
bitri.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
bitri  |-  ( ph  <->  ch )

Proof of Theorem bitri
StepHypRef Expression
1 bitri.1 . . . 4  |-  ( ph  <->  ps )
21biimpi 119 . . 3  |-  ( ph  ->  ps )
3 bitri.2 . . 3  |-  ( ps  <->  ch )
42, 3sylib 121 . 2  |-  ( ph  ->  ch )
53biimpri 132 . . 3  |-  ( ch 
->  ps )
65, 1sylibr 133 . 2  |-  ( ch 
->  ph )
74, 6impbii 125 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bitr2i  184  bitr3i  185  bitr4i  186  bitrd  187  3bitri  205  3bitr2i  207  3bitr3i  209  3bitr4i  211  bibi12i  228  imbi12i  238  pm4.71r  387  biadan2  451  anbi2ci  454  anbi12i  455  anbi12ci  456  pm5.3  466  an42  561  xchbinx  656  mt2bi  658  orbi12i  738  or42  746  pm5.53  776  orddi  794  anddi  795  pm2.1dc  807  dcim  811  notnotrdc  813  dcnnOLD  819  rbaib  891  rbaibr  892  pm4.43  918  orbididc  922  pm5.75  931  3orass  950  3anass  951  3ancomb  955  3anan32  958  3anan12  959  anandi3  960  anandi3r  961  xordc  1355  falbitru  1380  19.26-2  1443  19.26-3an  1444  alrot3  1446  albiim  1448  2albiim  1449  19.27h  1524  19.27  1525  19.28h  1526  19.28  1527  nfalt  1542  aaanh  1550  aaan  1551  alinexa  1567  19.21-2  1630  nf2  1631  19.44  1645  19.45  1646  exrot3  1653  exrot4  1654  eeor  1658  sbcof2  1766  sbid2h  1805  19.23vv  1840  sbnv  1844  sblimv  1850  pm11.53  1851  19.41vv  1859  19.41vvv  1860  19.41vvvv  1861  exdistrv  1864  19.42vv  1865  19.42vvv  1866  19.42vvvv  1867  4exdistr  1870  cbvex4v  1882  eean  1883  sbn  1903  sbim  1904  sbor  1905  sban  1906  sbrim  1907  sblim  1908  sbbi  1910  sblbis  1911  sbrbis  1912  sbrbif  1913  sbco2d  1917  sbco2vd  1918  sbnf2  1934  2sb5  1936  2sb6  1937  sbcom2v  1938  sbcom2v2  1939  sbcom2  1940  sb6a  1941  2sb5rf  1942  2sb6rf  1943  sbalyz  1952  sbal  1953  sbal1yz  1954  sbex  1957  sbalv  1958  sbco4lem  1959  exsb  1961  2exsb  1962  eujust  1979  euf  1982  cbveu  2001  mor  2019  eu2  2021  mo4f  2037  eu4  2039  2exeu  2069  2eu4  2070  exists1  2073  abid  2105  eleq12i  2185  abeq2  2226  abeq2i  2228  clabel  2243  abid2f  2283  sbabel  2284  neeq12i  2302  neanior  2372  ralnex  2403  dfrex2dc  2405  ralinexa  2439  nfraldya  2446  nfrexdya  2447  r3al  2454  r19.26-2  2538  ralbiim  2543  ralnex2  2548  r19.43  2566  ralcomf  2569  rexcomf  2570  rexrot4  2574  reean  2576  3reeanv  2578  rabbi  2585  cbvralf  2625  cbvrexf  2626  cbvreu  2629  cbvral2v  2639  cbvrex2v  2640  cbvral3v  2641  cbvralsv  2642  cbvrexsv  2643  sbralie  2644  rabeq2i  2657  issetf  2667  2gencl  2693  3gencl  2694  ceqsex2  2700  ceqsex3v  2702  ceqsex6v  2704  ceqsex8v  2705  gencbvex  2706  gencbval  2708  spc2gv  2750  eqvincf  2784  ceqsrex2v  2791  elrab2  2816  ralab  2817  ralrab  2818  rexab  2819  rexrab  2820  ralab2  2821  rexab2  2823  eueq3dc  2831  morex  2841  euind  2844  reu2  2845  reu6  2846  rmo4  2850  reu4  2851  reu7  2852  rmo3f  2854  rmo4f  2855  rmoim  2858  2reuswapdc  2861  reuind  2862  2rmorex  2863  sbcco  2903  sbccomlem  2955  sbccom  2956  ra5  2969  rmo3  2972  csbco  2984  sbnfc2  3030  csbabg  3031  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  dfss  3055  dfss2f  3058  ss2ab  3135  dfdif3  3156  difeqri  3166  ddifstab  3178  raldifb  3186  uneqri  3188  ssequn2  3219  unss  3220  rexun  3226  ralunb  3227  elin2  3234  ineqri  3239  dfss1  3250  dfss5  3251  dfss4st  3279  ssddif  3280  difin  3283  indif  3289  difundi  3298  indifdir  3302  symdifxor  3312  inrab2  3319  rabun2  3325  reuun2  3329  0el  3355  rabeq0  3362  abeq0  3363  disjr  3382  disj1  3383  undif4  3395  uneqdifeqim  3418  r19.2m  3419  r19.3rm  3421  r19.9rmv  3424  raaan  3439  pwss  3496  dfpr2  3516  ralsnsg  3531  ralsns  3532  eltpg  3539  ralprg  3544  rexprg  3545  raltpg  3546  rextpg  3547  snprc  3558  rabrsndc  3561  euabsn2  3562  eusn  3567  eldifsn  3620  ssdifsn  3621  rexdifsn  3625  eqsnm  3652  tpss  3655  snsssn  3658  prel12  3668  preqsn  3672  oprcl  3699  pwtpss  3703  eluniab  3718  elunirab  3719  unipr  3720  dfnfc2  3724  uniun  3725  uniin  3726  uni0b  3731  unissb  3736  elintab  3752  elintrab  3753  ssintab  3758  ssintrab  3764  intun  3772  intpr  3773  elrint  3781  iuncom4  3790  iuneq2  3799  dfiun2g  3815  ssiinf  3832  iundif2ss  3848  elriin  3853  iunxiun  3864  pwssb  3868  elpwpw  3869  iunpwss  3874  dfdisj2  3878  disjiun  3894  cbvopab1  3971  dftr5  3999  trint  4011  inex1  4032  inuni  4050  repizf2lem  4055  unidif0  4061  axpweq  4065  bnd2  4067  exmid01  4091  zfpair2  4102  exss  4119  elop  4123  opm  4126  otth  4134  copsex4g  4139  opeqsn  4144  opelopabsbALT  4151  brabga  4156  opelopabaf  4165  iunopab  4173  pwunss  4175  pocl  4195  frirrg  4242  elsuci  4295  elsucg  4296  sucel  4302  unisucg  4306  uniuni  4342  reusv3  4351  iunpw  4371  setindel  4423  elirr  4426  en2lp  4439  ordpwsucss  4452  zfregfr  4458  tfi  4466  peano2  4479  peano5  4482  elxp  4526  opelxp  4539  brxp  4540  rabxp  4546  opthprc  4560  brab2a  4562  opeliunxp  4564  xpundi  4565  xpundir  4566  elvvv  4572  brinxp  4577  brab2ga  4584  0xp  4589  ssrel2  4599  eqrelrel  4610  reliun  4630  reluni  4632  raliunxp  4650  rexiunxp  4651  ralxpf  4655  rexxpf  4656  iunxpf  4657  relop  4659  elco  4675  elcnv  4686  elcnv2  4687  dmin  4717  dmuni  4719  dmopab  4720  dmi  4724  dmmrnm  4728  rnopab  4756  elrnmpt1  4760  rncoeq  4782  resiexg  4834  dfima2  4853  dfima3  4854  elima2  4857  elima3  4858  imai  4865  elimasn  4876  epini  4880  dfse2  4882  cotr  4890  issref  4891  intasym  4893  asymref  4894  cnvopab  4910  cnvi  4913  cnvdif  4915  imainss  4924  rnxpid  4943  dfrel2  4959  dfrel3  4966  dmsnm  4974  rnsnm  4975  relsn2m  4979  dmsnopg  4980  cnvcnvsn  4985  elxp4  4996  elxp5  4997  cnvresima  4998  mptpreima  5002  dfco2  5008  coundi  5010  coundir  5011  imaco  5014  coiun  5018  coi1  5024  relssdmrn  5029  relrelss  5035  unixpm  5044  ressn  5049  cnviinm  5050  cnvpom  5051  cnvsom  5052  cbviota  5063  iotass  5075  dffun2  5103  dffun4  5104  dffun7  5120  dffun8  5121  dffun9  5122  funopab  5128  funun  5137  funcnvsn  5138  fntpg  5149  funcnv2  5153  funcnv  5154  fun2cnv  5157  fncnv  5159  fun11  5160  fununi  5161  imadiflem  5172  imadif  5173  imainlem  5174  funimaexglem  5176  fnunsn  5200  fnres  5209  fnopabg  5216  mptfng  5218  mptun  5224  fun  5265  fcnvres  5276  dff12  5297  f1cnvcnv  5309  funforn  5322  dff1o2  5340  dff1o5  5344  f1orn  5345  resdif  5357  ffoss  5367  f11o  5368  f1o00  5370  fo00  5371  elfv  5387  fv3  5412  nfvres  5422  eqfnfv3  5488  fneqeql  5496  unpreima  5513  respreima  5516  dffo3  5535  dffo5  5537  f1ompt  5539  ffnfvf  5547  fmptco  5554  ftpg  5572  fnressn  5574  idref  5626  abrexco  5628  dff13  5637  dff13f  5639  fliftel  5662  isoini  5687  eusvobj2  5728  acexmidlema  5733  acexmidlemb  5734  acexmidlemph  5735  acexmidlem2  5739  oprabid  5771  brabvv  5785  dfoprab2  5786  eqoprab2b  5797  dmoprab  5820  rnoprab  5822  eloprabga  5826  mpomptx  5830  resoprab  5835  ffnov  5843  elrnmpo  5852  ralrnmpo  5853  rexrnmpo  5854  ovid  5855  ovi3  5875  ov6g  5876  foov  5885  opabex3d  5987  opabex3  5988  abexssex  5991  oprabex3  5995  oprabrexex2  5996  fmpo  6067  xporderlem  6096  f1od2  6100  mpoxopovel  6106  brtpos2  6116  dmtpos  6121  tpostpos  6129  tpossym  6141  tposoprab  6145  dfsmo2  6152  tfrlem7  6182  tfrlem9  6184  tfr1onlemaccex  6213  tfrcllemaccex  6226  tfrcldm  6228  frecabex  6263  el1o  6302  dif1o  6303  dfer2  6398  brdifun  6424  eqerlem  6428  qsid  6462  iinerm  6469  riinerm  6470  erinxp  6471  brecop  6487  eroveu  6488  erovlem  6489  ecopovsym  6493  mapval2  6540  mapsn  6552  elixp  6567  ixpeq2  6574  ixpin  6585  ixpiinm  6586  mptelixpg  6596  ixpsnf1o  6598  domen  6613  isfi  6623  en1  6661  xpsnen  6683  xpcomco  6688  xpassen  6692  ssenen  6713  nneneq  6719  snnen2oprc  6722  ac6sfi  6760  exmidpw  6770  eldju  6921  djur  6922  eldju2ndl  6925  eldju2ndr  6926  finomni  6980  acfun  7031  ccfunen  7047  elni  7084  ltexpi  7113  enq0enq  7207  enq0ref  7209  enq0tr  7210  prarloclem3  7273  ltdfpr  7282  genpdflem  7283  genpassl  7300  genpassu  7301  nqprrnd  7319  nqprl  7327  nqpru  7328  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemdisj  7382  ltexprlemloc  7383  recexprlemdisj  7406  caucvgprprlemell  7461  caucvgprprlemelu  7462  suplocexprlemml  7492  suplocsrlemb  7582  opelcn  7602  elreal  7604  elreal2  7606  peano1nnnn  7628  axicn  7639  axaddf  7644  axmulf  7645  axprecex  7656  axpre-ltirr  7658  axpre-mulgt0  7663  axcaucvglemres  7675  axpre-suploc  7678  xrlenlt  7797  ltxrlt  7798  inelr  8313  reapcotr  8327  1nn  8695  elnnne0  8949  un0addcl  8968  un0mulcl  8969  elnnz  9022  elznn0nn  9026  elznn0  9027  elznn  9028  elz2  9080  zapne  9083  3halfnz  9106  prime  9108  raluz2  9330  rexuz2  9332  supinfneg  9346  infsupneg  9347  eluz2b2  9353  eluz2b3  9354  ublbneg  9361  elq  9370  qreccl  9390  ralrp  9418  rexrp  9419  rpnegap  9429  ltxr  9517  xrnemnf  9519  xrltso  9537  icc0r  9664  divelunit  9740  fzprval  9817  fztpval  9818  elfz1b  9825  fz01or  9846  4fvwrd4  9872  fzolb  9885  fzolb2  9886  elfzo3  9895  fzouzsplit  9911  elfzo0z  9916  fzo0m  9923  fzind2  9971  ioo0  9992  ico0  9994  ioc0  9995  uzennn  10164  seq3f1olemp  10230  caucvgre  10708  cvg1nlemcau  10711  resqrexlemex  10752  climeu  11020  fsum2dlemstep  11158  expcnv  11228  divides  11407  m1exp1  11510  divalgb  11534  bezoutlemnewy  11596  bezoutlemmain  11598  bezoutlemex  11601  dfgcd2  11614  lcmgcdlem  11670  isprm2  11710  isprm3  11711  isprm4  11712  sqrt2irr  11752  oddpwdc  11763  ennnfoneleminc  11835  ennnfonelemex  11838  ennnfonelemr  11847  ctiunct  11864  istps  12110  istps2  12111  isbasis2g  12123  tgval2  12131  txuni2  12336  tx1cn  12349  tx2cn  12350  uptx  12354  txdis1cn  12358  blres  12514  xmeterval  12515  xmeter  12516  isxms2  12532  isms2  12534  metrest  12586  qtopbasss  12601  dedekindicclemicc  12690  limcdifap  12711  pilem1  12771  sincosq1lem  12817  decidr  12899  bdcuni  12970  bdcriota  12977  bdinex1  12993  bj-zfpair2  13004  bj-axun2  13009  bj-ssom  13030  ss1oel2o  13085  nninfsellemdc  13102  nninfsellemsuc  13104  nninfsellemqall  13107
  Copyright terms: Public domain W3C validator