ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bitri Unicode 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  |-  ( 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 113 . . 3  |-  ( ph  ->  ps )
3 bitri.2 . . 3  |-  ( ps  <->  ch )
42, 3sylib 127 . 2  |-  ( ph  ->  ch )
53biimpri 124 . . 3  |-  ( ch 
->  ps )
65, 1sylibr 137 . 2  |-  ( ch 
->  ph )
74, 6impbii 117 1  |-  ( ph  <->  ch )
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  607  mt2bi  609  orbi12i  681  or42  689  pm5.53  715  orddi  733  anddi  734  pm2.1dc  745  notnotrdc  751  dcim  784  testbitestn  823  rbaib  830  rbaibr  831  pm4.43  856  orbididc  860  pm5.75  869  3orass  888  3anass  889  3ancomb  893  3anan32  896  3anan12  897  anandi3  898  anandi3r  899  xordc  1283  falbitru  1308  19.26-2  1371  19.26-3an  1372  alrot3  1374  albiim  1376  2albiim  1377  19.27h  1452  19.27  1453  19.28h  1454  19.28  1455  nfalt  1470  aaanh  1478  aaan  1479  alinexa  1494  19.21-2  1557  nf2  1558  19.44  1572  19.45  1573  exrot3  1580  exrot4  1581  eeor  1585  sbcof2  1691  sbid2h  1729  19.23vv  1764  sbnv  1768  sblimv  1774  pm11.53  1775  19.41vv  1783  19.41vvv  1784  19.41vvvv  1785  19.42vv  1788  19.42vvv  1789  19.42vvvv  1790  4exdistr  1793  cbvex4v  1805  eean  1806  sbn  1826  sbim  1827  sbor  1828  sban  1829  sbrim  1830  sblim  1831  sbbi  1833  sblbis  1834  sbrbis  1835  sbrbif  1836  sbco2d  1840  sbco2vd  1841  sbnf2  1857  2sb5  1859  2sb6  1860  sbcom2v  1861  sbcom2v2  1862  sbcom2  1863  sb6a  1864  2sb5rf  1865  2sb6rf  1866  sbalyz  1875  sbal  1876  sbal1yz  1877  sbex  1880  sbalv  1881  sbco4lem  1882  exsb  1884  2exsb  1885  eujust  1902  euf  1905  cbveu  1924  mor  1942  eu2  1944  mo4f  1960  eu4  1962  2exeu  1992  2eu4  1993  exists1  1996  abid  2028  eleq12i  2105  abeq2  2146  abeq2i  2148  clabel  2163  abid2f  2202  sbabel  2203  neeq12i  2222  neanior  2292  ralnex  2316  ralinexa  2351  nfraldya  2358  nfrexdya  2359  r3al  2366  r19.26-2  2442  ralbiim  2447  r19.43  2468  ralcomf  2471  rexcomf  2472  rexrot4  2476  reean  2478  3reeanv  2480  rabbi  2487  cbvralf  2527  cbvrexf  2528  cbvreu  2531  cbvral2v  2541  cbvrex2v  2542  cbvral3v  2543  cbvralsv  2544  cbvrexsv  2545  sbralie  2546  rabeq2i  2554  issetf  2562  2gencl  2587  3gencl  2588  ceqsex2  2594  ceqsex3v  2596  ceqsex6v  2598  ceqsex8v  2599  gencbvex  2600  gencbval  2602  spc2gv  2643  eqvincf  2669  ceqsrex2v  2676  elrab2  2700  ralab  2701  ralrab  2702  rexab  2703  rexrab  2704  ralab2  2705  rexab2  2707  eueq3dc  2715  morex  2725  euind  2728  reu2  2729  reu6  2730  rmo4  2734  reu4  2735  reu7  2736  rmoim  2740  2reuswapdc  2743  reuind  2744  2rmorex  2745  sbcco  2785  sbccomlem  2832  sbccom  2833  ra5  2846  rmo3  2849  csbco  2861  sbnfc2  2906  csbabg  2907  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  dfss  2932  dfss2f  2936  ss2ab  3008  dfpss2  3029  dfpss3  3030  psseq12i  3035  difeqri  3064  raldifb  3083  uneqri  3085  ssequn2  3116  unss  3117  rexun  3123  ralunb  3124  elin2  3127  ineqri  3130  dfss1  3141  dfss5  3142  nsspssun  3170  ssddif  3171  difin  3174  indif  3180  difundi  3189  indifdir  3193  symdifxor  3203  inrab2  3210  rabun2  3216  reuun2  3220  0el  3241  rabeq0  3247  abeq0  3248  0pss  3265  disjr  3269  disj1  3270  disj4im  3276  disjpss  3278  undif4  3284  uneqdifeqim  3308  r19.3rm  3310  r19.9rmv  3313  raaan  3327  pwss  3374  dfpr2  3394  ralsnsg  3407  ralsns  3408  rexsnsOLD  3410  eltpg  3416  ralprg  3421  rexprg  3422  raltpg  3423  rextpg  3424  snprc  3435  rabrsndc  3438  euabsn2  3439  eusn  3444  eldifsn  3495  rexdifsn  3499  eqsnm  3526  tpss  3529  snsssn  3532  prel12  3542  preqsn  3546  oprcl  3573  pwtpss  3577  eluniab  3592  elunirab  3593  unipr  3594  dfnfc2  3598  uniun  3599  uniin  3600  uni0b  3605  unissb  3610  elintab  3626  elintrab  3627  ssintab  3632  ssintrab  3638  intun  3646  intpr  3647  elrint  3655  iuncom4  3664  iuneq2  3673  dfiun2g  3689  ssiinf  3706  iundif2ss  3722  elriin  3727  iunxiun  3736  pwssb  3740  iunpwss  3743  dfdisj2  3747  cbvopab1  3830  dftr5  3857  trint  3869  inex1  3891  inuni  3909  repizf2lem  3914  unidif0  3920  axpweq  3924  bnd2  3926  zfpair2  3945  exss  3963  elop  3968  opm  3971  otth  3979  copsex4g  3984  opeqsn  3989  opelopabsbALT  3996  brabga  4001  opelopabaf  4010  iunopab  4018  pwunss  4020  pocl  4040  frirrg  4087  elsuci  4140  elsucg  4141  sucel  4147  unisucg  4151  uniuni  4183  reusv3  4192  iunpw  4211  setindel  4263  elirr  4266  en2lp  4278  ordpwsucss  4291  zfregfr  4298  tfi  4305  peano2  4318  peano5  4321  elxp  4362  opelxp  4374  brxp  4375  rabxp  4380  opthprc  4391  brab2a  4393  opeliunxp  4395  xpundi  4396  xpundir  4397  elvvv  4403  brinxp  4408  brab2ga  4415  0xp  4420  ssrel2  4430  eqrelrel  4441  reliun  4458  reluni  4460  raliunxp  4477  rexiunxp  4478  ralxpf  4482  rexxpf  4483  iunxpf  4484  relop  4486  elcnv  4512  elcnv2  4513  dmin  4543  dmuni  4545  dmopab  4546  dmi  4550  dmmrnm  4554  rnopab  4581  elrnmpt1  4585  rncoeq  4605  resiexg  4653  dfima2  4670  dfima3  4671  elima2  4674  elima3  4675  imai  4681  elimasn  4692  epini  4696  dfse2  4698  cotr  4706  issref  4707  intasym  4709  asymref  4710  cnvopab  4726  cnvi  4728  cnvdif  4730  imainss  4739  rnxpid  4755  dfrel2  4771  dfrel3  4778  dmsnm  4786  rnsnm  4787  relsn2m  4791  dmsnopg  4792  cnvcnvsn  4797  elxp4  4808  elxp5  4809  cnvresima  4810  mptpreima  4814  dfco2  4820  coundi  4822  coundir  4823  imaco  4826  coiun  4830  coi1  4836  relssdmrn  4841  relrelss  4844  unixpm  4853  ressn  4858  cnviinm  4859  cnvpom  4860  cnvsom  4861  cbviota  4872  iotass  4884  dffun2  4912  dffun4  4913  dffun7  4928  dffun8  4929  dffun9  4930  funopab  4935  funun  4944  funcnvsn  4945  fntpg  4955  funcnv2  4959  funcnv  4960  fun2cnv  4963  fncnv  4965  fun11  4966  fununi  4967  imadiflem  4978  imadif  4979  imainlem  4980  funimaexglem  4982  fnunsn  5006  fnres  5015  fnopabg  5022  mptfng  5024  mptun  5029  fun  5063  fcnvres  5073  dff12  5091  f1cnvcnv  5100  funforn  5113  dff1o2  5131  dff1o5  5135  f1orn  5136  resdif  5148  ffoss  5158  f11o  5159  f1o00  5161  fo00  5162  elfv  5176  fv3  5197  nfvres  5206  eqfnfv3  5267  fneqeql  5275  unpreima  5292  respreima  5295  dffo3  5314  dffo5  5316  f1ompt  5320  ffnfvf  5324  fmptco  5330  ftpg  5347  fnressn  5349  idref  5396  abrexco  5398  dff13  5407  dff13f  5409  fliftel  5433  isoini  5457  eusvobj2  5498  acexmidlema  5503  acexmidlemb  5504  acexmidlemph  5505  acexmidlem2  5509  oprabid  5537  brabvv  5551  dfoprab2  5552  eqoprab2b  5563  dmoprab  5585  rnoprab  5587  eloprabga  5591  mpt2mptx  5595  resoprab  5597  ffnov  5605  elrnmpt2  5614  ralrnmpt2  5615  rexrnmpt2  5616  ovid  5617  ovi3  5637  ov6g  5638  foov  5647  opabex3d  5748  opabex3  5749  abexssex  5752  oprabex3  5756  oprabrexex2  5757  fmpt2  5827  xporderlem  5852  mpt2xopovel  5856  brtpos2  5866  dmtpos  5871  tpostpos  5879  tpossym  5891  tposoprab  5895  dfsmo2  5902  tfrlem7  5933  tfrlem9  5935  frecabex  5984  el1o  6020  dif1o  6021  dfer2  6107  brdifun  6133  eqerlem  6137  qsid  6171  iinerm  6178  riinerm  6179  erinxp  6180  brecop  6196  eroveu  6197  erovlem  6198  ecopovsym  6202  domen  6232  isfi  6241  en1  6279  xpsnen  6295  xpcomco  6300  xpassen  6304  nneneq  6320  snnen2oprc  6323  ac6sfi  6352  elni  6406  ltexpi  6435  enq0enq  6529  enq0ref  6531  enq0tr  6532  prarloclem3  6595  ltdfpr  6604  genpdflem  6605  genpassl  6622  genpassu  6623  nqprrnd  6641  nqprl  6649  nqpru  6650  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemdisj  6704  ltexprlemloc  6705  recexprlemdisj  6728  caucvgprprlemell  6783  caucvgprprlemelu  6784  opelcn  6903  elreal  6905  elreal2  6907  peano1nnnn  6928  axicn  6939  axprecex  6954  axpre-ltirr  6956  axpre-mulgt0  6961  axcaucvglemres  6973  xrlenlt  7084  ltxrlt  7085  inelr  7575  reapcotr  7589  1nn  7925  elnnne0  8195  un0addcl  8215  un0mulcl  8216  elnnz  8255  elznn0nn  8259  elznn0  8260  elznn  8261  elz2  8312  zapne  8315  prime  8337  raluz2  8522  rexuz2  8524  eluz2b2  8540  eluz2b3  8541  ublbneg  8548  elq  8557  qreccl  8576  ralrp  8604  rexrp  8605  rpnegap  8615  ltxr  8695  xrnemnf  8699  xrltso  8717  icc0r  8795  divelunit  8870  fzprval  8944  fztpval  8945  elfz1b  8952  4fvwrd4  8997  fzolb  9009  fzolb2  9010  elfzo3  9019  fzouzsplit  9035  elfzo0z  9040  fzo0m  9047  fzind2  9095  caucvgre  9580  cvg1nlemcau  9583  resqrexlemex  9623  climeu  9817  sqrt2irr  9878  bdcuni  9996  bdcriota  10003  bdinex1  10019  bj-zfpair2  10030  bj-axun2  10035  bj-ssom  10060
  Copyright terms: Public domain W3C validator