Theorem bitr4i 187

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr4i.1	|- ( ph <-> ps )
bitr4i.2	|- ( ch <-> ps )

Assertion

Ref	Expression
bitr4i	|- ( ph <-> ch )

Proof of Theorem bitr4i

Step	Hyp	Ref	Expression
1		bitr4i.1	. 2 |- ( ph <-> ps )
2		bitr4i.2	. . 3 |- ( ch <-> ps )
3	2	bicomi 132	. 2 |- ( ps <-> ch )
4	1, 3	bitri 184	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr2i  208  3bitr2ri  209  3bitr4i  212  3bitr4ri  213  biancomi  270  imdistan  444  bianass  469  biadani  612  mpbiran  942  mpbiran2  943  3anrev  990  an6  1332  nfand  1579  19.33b2  1640  nf3  1680  nf4dc  1681  nf4r  1682  equsalh  1737  sb6x  1790  sb5f  1815  sbidm  1862  sb5  1899  sbanv  1901  sborv  1902  sbhb  1956  sb3an  1974  sbel2x  2014  sbal1yz  2017  sbexyz  2019  eu2  2086  2eu4  2135  cleqh  2293  cleqf  2361  dcne  2375  necon3bii  2402  ne3anior  2452  r2alf  2511  r2exf  2512  r19.23t  2601  r19.26-3  2624  r19.26m  2625  r19.43  2652  rabid2  2671  isset  2766  ralv  2777  rexv  2778  reuv  2779  rmov  2780  rexcom4b  2785  ceqsex4v  2803  ceqsex8v  2805  ceqsrexv  2890  ralrab2  2925  rexrab2  2927  reu2  2948  reu3  2950  reueq  2959  2reuswapdc  2964  reuind  2965  sbc3an  3047  rmo2ilem  3075  csbcow  3091  dfss2  3168  dfss3  3169  dfss3f  3171  ssabral  3250  rabss  3256  ssrabeq  3266  uniiunlem  3268  dfdif3  3269  ddifstab  3291  uncom  3303  inass  3369  indi  3406  difindiss  3413  difin2  3421  reupick3  3444  n0rf  3459  eq0  3465  eqv  3466  vss  3494  disj  3495  disj3  3499  undisj1  3504  undisj2  3505  exsnrex  3660  euabsn2  3687  euabsn  3688  prssg  3775  dfuni2  3837  unissb  3865  elint2  3877  ssint  3886  dfiin2g  3945  iunn0m  3973  iunxun  3992  iunxiun  3994  iinpw  4003  disjnim  4020  dftr2  4129  dftr5  4130  dftr3  4131  dftr4  4132  vnex  4160  inuni  4184  snelpw  4242  sspwb  4245  opelopabsb  4290  eusv2  4488  orddif  4579  onintexmid  4605  zfregfr  4606  tfi  4614  opthprc  4710  elxp3  4713  xpiundir  4718  elvv  4721  brinxp2  4726  relsn  4764  reliun  4780  inxp  4796  raliunxp  4803  rexiunxp  4804  cnvuni  4848  dm0rn0  4879  elrn  4905  ssdmres  4964  dfres2  4994  dfima2  5007  args  5034  cotr  5047  intasym  5050  asymref  5051  intirr  5052  cnv0  5069  xp11m  5104  cnvresima  5155  resco  5170  rnco  5172  coiun  5175  coass  5184  dfiota2  5216  dffun2  5264  dffun6f  5267  dffun4f  5270  dffun7  5281  dffun9  5283  funfn  5284  svrelfun  5319  imadiflem  5333  dffn2  5405  dffn3  5414  fintm  5439  dffn4  5482  dff1o4  5508  brprcneu  5547  eqfnfv3  5657  fnreseql  5668  fsn  5730  abrexco  5802  imaiun  5803  mpo2eqb  6028  elovmpo  6117  abexex  6178  releldm2  6238  fnmpo  6255  dftpos4  6316  tfrlem7  6370  0er  6621  eroveu  6680  erovlem  6681  map0e  6740  elixpconst  6760  domen  6805  reuen1  6855  xpf1o  6900  ssfilem  6931  finexdc  6958  pw1dc0el  6967  ssfirab  6990  sbthlemi10  7025  djuexb  7103  dmaddpq  7439  dmmulpq  7440  distrnqg  7447  enq0enq  7491  enq0tr  7494  nqnq0pi  7498  distrnq0  7519  prltlu  7547  prarloc  7563  genpdflem  7567  ltexprlemm  7660  ltexprlemlol  7662  ltexprlemupu  7664  ltexprlemdisj  7666  recexprlemdisj  7690  ltresr  7899  elnnz  9327  dfz2  9389  2rexuz  9647  eluz2b1  9666  elxr  9842  elixx1  9963  elioo2  9987  elioopnf  10033  elicopnf  10035  elfz1  10079  fzdifsuc  10147  fznn  10155  fzp1nel  10170  fznn0  10179  dfrp2  10332  redivap  11018  imdivap  11025  rexanre  11364  climreu  11440  prodmodc  11721  3dvdsdec  12006  3dvds2dec  12007  bezoutlembi  12142  nnwosdc  12176  isprm2  12255  isprm3  12256  isprm4  12257  pythagtriplem2  12404  elgz  12509  inffinp1  12586  isnsg4  13282  isrng  13430  isring  13496  dfrhm2  13650  lss1d  13879  isbasis3g  14214  restsn  14348  lmbr  14381  txbas  14426  tx2cn  14438  elcncf1di  14734  dedekindicclemicc  14786  limcrcl  14812  bj-nnor  15226  bj-vprc  15388  ss1oel2o  15484  subctctexmid  15491  trirec0xor  15535