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  576  xchbinx  671  mt2bi  673  orbi12i  753  or42  761  pm5.53  791  orddi  809  anddi  810  pm2.1dc  822  dcim  826  notnotrdc  828  dcnnOLD  834  rbaib  906  rbaibr  907  pm4.43  933  orbididc  937  pm5.75  946  3orass  965  3anass  966  3ancomb  970  3anan32  973  3anan12  974  anandi3  975  anandi3r  976  xordc  1370  falbitru  1395  19.26-2  1458  19.26-3an  1459  alrot3  1461  albiim  1463  2albiim  1464  19.27h  1539  19.27  1540  19.28h  1541  19.28  1542  nfalt  1557  aaanh  1565  aaan  1566  alinexa  1582  19.21-2  1645  nf2  1646  19.44  1660  19.45  1661  exrot3  1668  exrot4  1669  eeor  1673  sbcof2  1782  sbid2h  1821  19.23vv  1856  sbnv  1860  sblimv  1866  pm11.53  1867  19.41vv  1875  19.41vvv  1876  19.41vvvv  1877  exdistrv  1882  19.42vv  1883  19.42vvv  1884  19.42vvvv  1885  4exdistr  1888  cbvex4v  1902  eean  1903  sbn  1925  sbim  1926  sbor  1927  sban  1928  sbrim  1929  sblim  1930  sbbi  1932  sblbis  1933  sbrbis  1934  sbrbif  1935  sbco2d  1939  sbco2vd  1940  sbnf2  1956  2sb5  1958  2sb6  1959  sbcom2v  1960  sbcom2v2  1961  sbcom2  1962  sb6a  1963  2sb5rf  1964  2sb6rf  1965  sbalyz  1974  sbal  1975  sbal1yz  1976  sbex  1979  sbalv  1980  sbco4lem  1981  exsb  1983  2exsb  1984  eujust  2001  euf  2004  cbveu  2023  mor  2041  eu2  2043  mo4f  2059  eu4  2061  2exeu  2091  2eu4  2092  exists1  2095  abid  2127  eleq12i  2207  abeq2  2248  abeq2i  2250  clabel  2266  abid2f  2306  sbabel  2307  neeq12i  2325  neanior  2395  ralnex  2426  dfrex2dc  2428  ralinexa  2462  nfraldya  2469  nfrexdya  2470  r3al  2477  r19.26-2  2561  ralbiim  2566  ralnex2  2571  r19.43  2589  ralcomf  2592  rexcomf  2593  rexrot4  2597  reean  2599  3reeanv  2601  rabbi  2608  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvral2v  2665  cbvrex2v  2666  cbvral3v  2667  cbvralsv  2668  cbvrexsv  2669  sbralie  2670  rabeq2i  2683  issetf  2693  2gencl  2719  3gencl  2720  ceqsex2  2726  ceqsex3v  2728  ceqsex6v  2730  ceqsex8v  2731  gencbvex  2732  gencbval  2734  spc2gv  2776  eqvincf  2810  ceqsrex2v  2817  elrab2  2843  ralab  2844  ralrab  2845  rexab  2846  rexrab  2847  ralab2  2848  rexab2  2850  eueq3dc  2858  morex  2868  euind  2871  reu2  2872  reu6  2873  rmo4  2877  reu4  2878  reu7  2879  rmo3f  2881  rmo4f  2882  rmoim  2885  2reuswapdc  2888  reuind  2889  2rmorex  2890  sbcco  2930  sbccomlem  2983  sbccom  2984  ra5  2997  rmo3  3000  csbco  3013  sbnfc2  3060  csbabg  3061  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  dfss  3085  dfss2f  3088  ss2ab  3165  dfdif3  3186  difeqri  3196  ddifstab  3208  raldifb  3216  uneqri  3218  ssequn2  3249  unss  3250  rexun  3256  ralunb  3257  elin2  3264  ineqri  3269  dfss1  3280  dfss5  3281  dfss4st  3309  ssddif  3310  difin  3313  indif  3319  difundi  3328  indifdir  3332  symdifxor  3342  inrab2  3349  rabun2  3355  reuun2  3359  0el  3385  rabeq0  3392  abeq0  3393  disjr  3412  disj1  3413  undif4  3425  uneqdifeqim  3448  r19.2m  3449  r19.3rm  3451  r19.9rmv  3454  raaan  3469  pwss  3526  dfpr2  3546  ralsnsg  3561  ralsns  3562  eltpg  3569  ralprg  3574  rexprg  3575  raltpg  3576  rextpg  3577  snprc  3588  rabrsndc  3591  euabsn2  3592  eusn  3597  eldifsn  3650  ssdifsn  3651  rexdifsn  3655  eqsnm  3682  tpss  3685  snsssn  3688  prel12  3698  preqsn  3702  oprcl  3729  pwtpss  3733  eluniab  3748  elunirab  3749  unipr  3750  dfnfc2  3754  uniun  3755  uniin  3756  uni0b  3761  unissb  3766  elintab  3782  elintrab  3783  ssintab  3788  ssintrab  3794  intun  3802  intpr  3803  elrint  3811  iuncom4  3820  iuneq2  3829  dfiun2g  3845  ssiinf  3862  iundif2ss  3878  elriin  3883  iunxiun  3894  pwssb  3898  elpwpw  3899  iunpwss  3904  dfdisj2  3908  disjiun  3924  cbvopab1  4001  dftr5  4029  trint  4041  inex1  4062  inuni  4080  repizf2lem  4085  unidif0  4091  axpweq  4095  bnd2  4097  exmid01  4121  zfpair2  4132  exss  4149  elop  4153  opm  4156  otth  4164  copsex4g  4169  opeqsn  4174  opelopabsbALT  4181  brabga  4186  opelopabaf  4195  iunopab  4203  pwunss  4205  pocl  4225  frirrg  4272  elsuci  4325  elsucg  4326  sucel  4332  unisucg  4336  uniuni  4372  reusv3  4381  iunpw  4401  setindel  4453  elirr  4456  en2lp  4469  ordpwsucss  4482  zfregfr  4488  tfi  4496  peano2  4509  peano5  4512  elxp  4556  opelxp  4569  brxp  4570  rabxp  4576  opthprc  4590  brab2a  4592  opeliunxp  4594  xpundi  4595  xpundir  4596  elvvv  4602  brinxp  4607  brab2ga  4614  0xp  4619  ssrel2  4629  eqrelrel  4640  reliun  4660  reluni  4662  raliunxp  4680  rexiunxp  4681  ralxpf  4685  rexxpf  4686  iunxpf  4687  relop  4689  elco  4705  elcnv  4716  elcnv2  4717  dmin  4747  dmuni  4749  dmopab  4750  dmi  4754  dmmrnm  4758  rnopab  4786  elrnmpt1  4790  rncoeq  4812  resiexg  4864  dfima2  4883  dfima3  4884  elima2  4887  elima3  4888  imai  4895  elimasn  4906  epini  4910  dfse2  4912  cotr  4920  issref  4921  intasym  4923  asymref  4924  cnvopab  4940  cnvi  4943  cnvdif  4945  imainss  4954  rnxpid  4973  dfrel2  4989  dfrel3  4996  dmsnm  5004  rnsnm  5005  relsn2m  5009  dmsnopg  5010  cnvcnvsn  5015  elxp4  5026  elxp5  5027  cnvresima  5028  mptpreima  5032  dfco2  5038  coundi  5040  coundir  5041  imaco  5044  coiun  5048  coi1  5054  relssdmrn  5059  relrelss  5065  unixpm  5074  ressn  5079  cnviinm  5080  cnvpom  5081  cnvsom  5082  cbviota  5093  iotass  5105  dffun2  5133  dffun4  5134  dffun7  5150  dffun8  5151  dffun9  5152  funopab  5158  funun  5167  funcnvsn  5168  fntpg  5179  funcnv2  5183  funcnv  5184  fun2cnv  5187  fncnv  5189  fun11  5190  fununi  5191  imadiflem  5202  imadif  5203  imainlem  5204  funimaexglem  5206  fnunsn  5230  fnres  5239  fnopabg  5246  mptfng  5248  mptun  5254  fun  5295  fcnvres  5306  dff12  5327  f1cnvcnv  5339  funforn  5352  dff1o2  5372  dff1o5  5376  f1orn  5377  resdif  5389  ffoss  5399  f11o  5400  f1o00  5402  fo00  5403  elfv  5419  fv3  5444  nfvres  5454  eqfnfv3  5520  fneqeql  5528  unpreima  5545  respreima  5548  dffo3  5567  dffo5  5569  f1ompt  5571  ffnfvf  5579  fmptco  5586  ftpg  5604  fnressn  5606  idref  5658  abrexco  5660  dff13  5669  dff13f  5671  fliftel  5694  isoini  5719  eusvobj2  5760  acexmidlema  5765  acexmidlemb  5766  acexmidlemph  5767  acexmidlem2  5771  oprabid  5803  brabvv  5817  dfoprab2  5818  eqoprab2b  5829  dmoprab  5852  rnoprab  5854  eloprabga  5858  mpomptx  5862  resoprab  5867  ffnov  5875  elrnmpo  5884  ralrnmpo  5885  rexrnmpo  5886  ovid  5887  ovi3  5907  ov6g  5908  foov  5917  opabex3d  6019  opabex3  6020  abexssex  6023  oprabex3  6027  oprabrexex2  6028  fmpo  6099  xporderlem  6128  f1od2  6132  mpoxopovel  6138  brtpos2  6148  dmtpos  6153  tpostpos  6161  tpossym  6173  tposoprab  6177  dfsmo2  6184  tfrlem7  6214  tfrlem9  6216  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfrcldm  6260  frecabex  6295  el1o  6334  dif1o  6335  dfer2  6430  brdifun  6456  eqerlem  6460  qsid  6494  iinerm  6501  riinerm  6502  erinxp  6503  brecop  6519  eroveu  6520  erovlem  6521  ecopovsym  6525  mapval2  6572  mapsn  6584  elixp  6599  ixpeq2  6606  ixpin  6617  ixpiinm  6618  mptelixpg  6628  ixpsnf1o  6630  domen  6645  isfi  6655  en1  6693  xpsnen  6715  xpcomco  6720  xpassen  6724  ssenen  6745  nneneq  6751  snnen2oprc  6754  ac6sfi  6792  exmidpw  6802  eldju  6953  djur  6954  eldju2ndl  6957  eldju2ndr  6958  finomni  7012  acfun  7070  ccfunen  7086  elni  7130  ltexpi  7159  enq0enq  7253  enq0ref  7255  enq0tr  7256  prarloclem3  7319  ltdfpr  7328  genpdflem  7329  genpassl  7346  genpassu  7347  nqprrnd  7365  nqprl  7373  nqpru  7374  ltexprlemopl  7423  ltexprlemopu  7425  ltexprlemdisj  7428  ltexprlemloc  7429  recexprlemdisj  7452  caucvgprprlemell  7507  caucvgprprlemelu  7508  suplocexprlemml  7538  suplocsrlemb  7628  opelcn  7648  elreal  7650  elreal2  7652  peano1nnnn  7674  axicn  7685  axaddf  7690  axmulf  7691  axprecex  7702  axpre-ltirr  7704  axpre-mulgt0  7709  axcaucvglemres  7721  axpre-suploc  7724  xrlenlt  7843  ltxrlt  7844  inelr  8360  reapcotr  8374  1nn  8745  elnnne0  9005  un0addcl  9024  un0mulcl  9025  elnnz  9078  elznn0nn  9082  elznn0  9083  elznn  9084  elz2  9136  zapne  9139  3halfnz  9162  prime  9164  raluz2  9388  rexuz2  9390  supinfneg  9404  infsupneg  9405  eluz2b2  9411  eluz2b3  9412  ublbneg  9419  elq  9428  qreccl  9448  ralrp  9477  rexrp  9478  rpnegap  9488  ltxr  9576  xrnemnf  9578  xrltso  9596  icc0r  9723  divelunit  9799  fzprval  9876  fztpval  9877  elfz1b  9884  fz01or  9905  4fvwrd4  9931  fzolb  9944  fzolb2  9945  elfzo3  9954  fzouzsplit  9970  elfzo0z  9975  fzo0m  9982  fzind2  10030  ioo0  10051  ico0  10053  ioc0  10054  uzennn  10223  seq3f1olemp  10289  caucvgre  10767  cvg1nlemcau  10770  resqrexlemex  10811  climeu  11079  fsum2dlemstep  11217  expcnv  11287  divides  11508  m1exp1  11611  divalgb  11635  bezoutlemnewy  11697  bezoutlemmain  11699  bezoutlemex  11702  dfgcd2  11715  lcmgcdlem  11771  isprm2  11811  isprm3  11812  isprm4  11813  sqrt2irr  11853  oddpwdc  11865  ennnfoneleminc  11937  ennnfonelemex  11940  ennnfonelemr  11949  ctiunct  11966  istps  12215  istps2  12216  isbasis2g  12228  tgval2  12236  txuni2  12441  tx1cn  12454  tx2cn  12455  uptx  12459  txdis1cn  12463  blres  12619  xmeterval  12620  xmeter  12621  isxms2  12637  isms2  12639  metrest  12691  qtopbasss  12706  dedekindicclemicc  12795  limcdifap  12816  pilem1  12884  sincosq1lem  12930  decidr  13110  bdcuni  13181  bdcriota  13188  bdinex1  13204  bj-zfpair2  13215  bj-axun2  13220  bj-ssom  13241  ss1oel2o  13296  nninfsellemdc  13315  nninfsellemsuc  13317  nninfsellemqall  13320  trirec0xor  13347
  Copyright terms: Public domain W3C validator