Theorem bitri 240

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

Step	Hyp	Ref	Expression
1		bitri.1	. . . 4 |- (ph <-> ps)
2	1	biimpi 186	. . 3 |- (ph -> ps)
3		bitri.2	. . 3 |- (ps <-> ch)
4	2, 3	sylib 188	. 2 |- (ph -> ch)
5	3	biimpri 197	. . 3 |- (ch -> ps)
6	5, 1	sylibr 203	. 2 |- (ch -> ph)
7	4, 6	impbii 180	1 |- (ph <-> ch)

Syntax hints:   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bitr2i  241  bitr3i  242  bitr4i  243  bitrd  244  3bitri  262  3bitr2i  264  3bitr3i  266  3bitr4i  268  xchbinx  301  bibi12i  306  imbi12i  316  mt2bi  328  iman  413  orbi12i  507  or42  515  pm4.71r  612  biadan2  623  anbi2ci  677  anbi12i  678  anbi12ci  679  pm5.3  692  pm5.53  771  an42  798  orddi  839  anddi  840  rbaib  873  rbaibr  874  pm4.43  893  biluk  899  pm5.75  903  dn1  932  3orass  937  3anass  938  3ancomb  943  3anan32  946  3anan12  947  3anor  948  an6  1261  xor2  1310  falbitru  1352  falnantru  1356  truxortru  1358  truxorfal  1359  falxorfal  1361  exp3acom23g  1371  hadass  1386  hadbi  1387  hadrot  1390  cador  1391  cadan  1392  cadnot  1394  cadcomb  1396  cadrot  1397  cad1  1398  had1  1402  alex  1572  alinexa  1578  alexn  1579  exanali  1585  19.26-2  1594  19.26-3an  1595  albiim  1611  2albiim  1612  ax12bOLD  1690  alrot3  1738  alrot4  1739  exrot3  1744  exrot4  1745  19.21-2  1864  nf2  1866  19.27  1869  19.28  1870  19.36  1871  19.37  1873  19.44  1877  19.45  1878  aaan  1884  eeor  1885  19.23vv  1892  pm11.53  1893  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  19.42vv  1907  19.42vvv  1908  4exdistr  1911  eean  1912  cbvex4v  2012  sbor  2066  sbrim  2067  sblim  2068  sban  2069  sbbi  2071  sblbis  2072  sbrbis  2073  sbrbif  2074  sbid2  2084  sbco2d  2087  sb8e  2093  sbnf2  2108  2sb5  2112  2sb6  2113  sbcom2  2114  sb6a  2116  2sb5rf  2117  2sb6rf  2118  sbex  2128  sbalv  2129  exsbOLD  2131  2exsb  2132  eujust  2206  euf  2210  cbveu  2224  eu2  2229  mo2  2233  sbmo  2234  mo3  2235  mo4f  2236  eu4  2243  moanim  2260  2mo  2282  2mos  2283  2eu1  2284  2eu3  2286  2eu4  2287  2eu6  2289  exists1  2293  abid  2341  eleq12i  2418  abeq2  2459  abeq2i  2461  clabel  2475  abid2f  2515  sbabel  2516  neeq12i  2529  necon1abii  2568  neanior  2602  ralnex  2625  rexnal  2626  ralinexa  2660  rexanali  2661  r3al  2672  r19.26-2  2748  ralbiim  2752  r19.30  2757  ralcomf  2770  rexcomf  2771  rexrot4  2775  reean  2778  3reeanv  2780  rabbi  2790  cbvralf  2830  cbvreu  2834  cbvral2v  2844  cbvrex2v  2845  cbvral3v  2846  cbvralsv  2847  cbvrexsv  2848  sbralie  2849  rabeq2i  2857  issetf  2865  2gencl  2889  3gencl  2890  ceqsex2  2896  ceqsex3v  2898  ceqsex6v  2900  ceqsex8v  2901  gencbvex  2902  spc3gv  2945  eqvincf  2968  ceqsrex2v  2975  elrab2  2997  ralab  2998  ralrab  2999  rexab  3000  rexrab  3001  ralab2  3002  rexab2  3004  eueq3  3012  morex  3021  euxfr2  3022  euxfr  3023  euind  3024  reu2  3025  reu6  3026  rmo4  3030  reu4  3031  reu7  3032  rmoim  3036  2reuswap  3039  reuind  3040  2reu5lem1  3042  2reu5lem2  3043  2reu5  3045  sbcco  3069  sbccomlem  3117  sbccom  3118  ra5  3131  rmo3  3134  csbco  3146  sbnfc2  3197  csbabg  3198  cbvralcsf  3199  cbvreucsf  3201  elsymdif  3224  dfss  3261  dfss2  3263  dfss2f  3265  ss2ab  3335  dfpss2  3355  dfpss3  3356  psseq12i  3361  sspsstri  3372  difeqri  3388  uneqri  3407  ssequn2  3437  unss  3438  rexun  3444  ralunb  3445  elin2  3447  ineqri  3450  dfss1  3461  dfss5  3462  nsspssun  3489  indifdir  3512  inrab2  3529  rabun2  3535  reuun2  3539  eq0  3565  0el  3567  abn0  3569  0pss  3589  disjr  3593  disj1  3594  disjpss  3602  undif4  3608  difin0ss  3617  inssdif0  3618  uneqdifeq  3639  r19.3rz  3642  r19.3rzv  3644  ralidm  3654  pwss  3737  dfpr2  3750  ralsns  3764  rexsns  3765  eltpg  3770  ralprg  3776  rexprg  3777  raltpg  3778  rextpg  3779  euabsn2  3792  eusn  3797  eldifsn  3840  rexdifsn  3844  difsnpss  3852  pwpw0  3856  ssunsn  3867  eqsn  3868  sstp  3871  tpss  3872  pwsnALT  3883  pwtp  3885  dfpss4  3889  eluniab  3904  elunirab  3905  unipr  3906  dfnfc2  3910  uniun  3911  uniin  3912  unissb  3922  elintab  3938  elintrab  3939  ssintab  3944  ssintrab  3950  intun  3959  intpr  3960  elrint  3968  iuncom4  3977  iuneq2  3986  dfiun2g  4000  ssiinf  4016  elriin  4039  iunxiun  4049  pwssb  4053  iunpwss  4056  ssofss  4077  axprimlem1  4089  axprimlem2  4090  axcnvprim  4092  axssetprim  4093  axsiprim  4094  axtyplowerprim  4095  axins2prim  4096  axins3prim  4097  ninexg  4098  snex  4112  pwadjoin  4120  elopk  4130  1cex  4143  elpw1  4145  snelpw1  4147  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  0nel1c  4160  eqpw1  4163  pw1un  4164  pw111  4171  ssrelk  4212  eqrelk  4213  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  elp6  4264  opksnelsik  4266  opkelimagekg  4272  cnvkxpk  4277  inxpk  4278  elimaksn  4284  cokrelk  4285  xpkvexg  4286  cnvkexg  4287  p6exg  4291  ssetkex  4295  sikexlem  4296  sikexg  4297  dfimak2  4299  insklem  4305  ins2kexg  4306  ins3kexg  4307  dfidk2  4314  dfuni3  4316  dfint3  4319  ndisjrelk  4324  dfpw2  4328  cbviota  4345  dfiota4  4373  dfaddc2  4382  dfnnc2  4396  0nelsuc  4401  peano1  4403  peano2  4404  addccom  4407  peano5  4410  nnc0suc  4413  elsuc  4414  addcass  4416  elfin  4421  el0c  4422  nnsucelrlem1  4425  nnsucelrlem2  4426  nnsucelr  4429  nndisjeq  4430  preaddccan2lem1  4455  ltfinex  4465  ltfintrilem1  4466  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  ncfinlower  4484  nnpw1ex  4485  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  evenodddisj  4517  nnadjoinlem1  4520  nnadjoin  4521  nnpweqlem1  4523  nnpweq  4524  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  tfinnn  4535  spfinex  4538  spfinsfincl  4540  vfinspsslem1  4551  vfinspss  4552  vfinspclt  4553  vfinncsp  4555  dfphi2  4570  dfop2lem1  4574  dfop2lem2  4575  dfop2  4576  dfproj22  4578  phi011lem1  4599  phi011  4600  proj2op  4602  eqvinop  4607  copsex4g  4611  eqop  4612  phidisjnn  4616  phialllem1  4617  phiall  4619  cbvopab1  4633  brabga  4702  opelopabaf  4711  opabn0  4717  el1st  4730  br1stg  4731  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem6  4737  setconslem7  4738  df1st2  4739  elswap  4741  dfswap2  4742  dfima2  4746  dfco1  4749  dfsi2  4752  elima2  4756  elima3  4757  dfid3  4769  elxp  4802  opelxp  4812  brxp  4813  rabxp  4815  opeliunxp  4821  eliunxp  4822  raliunxp  4824  rexiunxp  4825  ralxpf  4828  rexxpf  4829  iunxpf  4830  xpundi  4833  xpundir  4834  brinxp2  4836  brinxp  4837  xp0r  4843  ssopr  4847  eqopr  4848  brswap2  4861  elcnv  4890  elcnv2  4891  cnvco  4895  elrn2  4898  eldm  4899  eldm2  4900  dmun  4913  dmin  4914  dmuni  4915  dmopab  4916  dmi  4920  elimapw1  4945  elimapw12  4946  elimapw13  4947  elimapw11c  4949  dfima3  4952  dfima4  4953  rnopab  4968  rneq0  4971  dmcoss  4972  dmcosseq  4974  rncoeq  4976  dmres  4987  resabs1  4993  elres  4996  dfres2  5003  imai  5011  epini  5022  cotr  5027  intasym  5029  intirr  5030  cnvopab  5031  cnvi  5033  imainss  5043  cnvcnv  5063  dmsnn0  5065  rnsnn0  5066  dmsnopg  5067  cnvsn  5074  rnsnop  5076  cnvresima  5078  dfco2  5081  dfco2a  5082  coundi  5083  coundir  5084  coiun  5091  co01  5094  coi1  5095  dfcnv2  5101  elxp4  5109  df2nd2  5112  dfxp2  5114  cnviin  5119  dffun2  5120  dffun3  5121  dffun4  5122  dffun5  5123  dffun8  5135  dffun9  5136  nfunv  5139  funopab  5140  funun  5147  funsn  5148  funcnv2  5156  funcnv  5157  fncnv  5159  fun11  5160  fununi  5161  imadif  5172  fnunsn  5191  fnres  5200  iunfopab  5205  fnopabg  5206  fnopab2g  5207  fun  5237  fcnvres  5244  dff12  5258  funforn  5277  dff1o2  5292  dff1o3  5293  dff1o5  5296  f1ocnvb  5299  resdif  5307  f1ococnv2  5310  ffoss  5315  f11o  5316  f1o00  5318  fo00  5319  elfv  5327  fv3  5342  nfvres  5353  fnrnfv  5365  dmfco  5382  eqfnfv3  5395  unpreima  5409  respreima  5411  fnasrn  5418  dff4  5422  dffo3  5423  dffo5  5425  ffnfvf  5429  fopabfv  5431  fsn2  5435  fconst3  5458  fconst4  5459  funfvima  5460  abrexco  5464  funiunfv  5468  dff13  5472  dff13f  5473  isocnv2  5493  isomin  5497  isoini  5498  opbr1st  5502  opbr2nd  5503  dfid4  5504  swapf1o  5512  xpnedisj  5514  dmsi  5520  oprabid  5551  dfoprab2  5559  dmoprab  5575  rnoprab  5577  eloprabga  5579  resoprab  5582  ffnov  5588  fnov  5592  fov  5593  ovidig  5594  ov3  5600  ov6g  5601  foov  5607  ndmovcl  5615  ndmov  5616  ndmovdistr  5620  mptpreima  5683  mpt2mptx  5709  fmpt2  5732  brsnsi  5774  brsnsi1  5776  brsnsi2  5777  brco1st  5778  brco2nd  5779  trtxp  5782  brtxp  5784  restxp  5787  elfix  5788  otelins2  5792  otelins3  5793  brimage  5794  oqelins4  5795  dmtxp  5803  txpcofun  5804  otsnelsi3  5806  releqel  5808  releqmpt  5809  releqmpt2  5810  cupex  5817  composeex  5821  disjex  5824  addcfnex  5825  epprc  5828  funsex  5829  fnsex  5833  qrpprod  5837  brpprod  5840  dmpprod  5841  fnpprod  5844  brcrossg  5849  crossex  5851  pw1fnex  5853  pw1fnf1o  5856  fnfullfunlem1  5857  fvfullfunlem3  5864  domfnex  5871  ranfnex  5872  clos1ex  5877  clos1conn  5880  clos1induct  5881  clos1is  5882  dfnnc3  5886  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  ersymtr  5933  porta  5934  sopc  5935  frds  5936  weds  5939  eqerlem  5961  qsexg  5983  qsid  5991  mapexi  6004  pmvalg  6011  mapval2  6019  enex  6032  xpassenlem  6057  xpassen  6058  enpw1lem1  6062  enmap2lem1  6064  enmap2lem4  6067  enmap1lem1  6070  enmap1lem4  6073  enpw1pw  6076  enprmaplem1  6077  enprmaplem4  6080  nenpw1pwlem1  6085  brltc  6115  lecex  6116  elncs  6120  elnc  6126  ovmuc  6131  mucex  6134  1cnc  6140  peano4nc  6151  ncssfin  6152  ncspw1eu  6160  ovcelem1  6172  ceexlem1  6174  ceex  6175  fnce  6177  ce0nnul  6178  ce0nn  6181  fce  6189  el2c  6192  lec0cg  6199  sbthlem1  6204  sbth  6207  addlec  6209  nc0le1  6217  leconnnc  6219  dflec3  6222  nclenc  6223  lenc  6224  tc11  6229  taddc  6230  letc  6232  tcfnex  6245  nclennlem1  6249  muc0or  6253  csucex  6260  nnltp1clem1  6262  addccan2nclem1  6264  addccan2nclem2  6265  nmembers1lem1  6269  nmembers1lem2  6270  nmembers1lem3  6271  ltcirr  6273  nncdiv3lem1  6276  nncdiv3lem2  6277  nncdiv3  6278  nnc3n3p1  6279  nnc3n3p2  6280  spacvallem1  6282  spacind  6288  spacis  6289  nchoicelem6  6295  nchoicelem8  6297  nchoicelem9  6298  nchoicelem10  6299  nchoicelem11  6300  nchoicelem12  6301  nchoicelem14  6303  nchoicelem16  6305  nchoicelem18  6307  nchoicelem19  6308  dmfrec  6317  fnfreclem1  6318  scancan  6332