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  616  mpbiran  949  mpbiran2  950  3anrev  1015  an6  1358  nfand  1617  19.33b2  1678  nf3  1717  nf4dc  1718  nf4r  1719  equsalh  1774  sb6x  1827  sb5f  1852  sbidm  1899  sb5  1936  sbanv  1938  sborv  1939  sbhb  1993  sb3an  2011  sbel2x  2051  sbal1yz  2054  sbexyz  2056  eu2  2124  2eu4  2173  cleqh  2331  cleqf  2400  dcne  2414  necon3bii  2441  ne3anior  2491  r2alf  2550  r2exf  2551  r19.23t  2641  r19.26-3  2664  r19.26m  2665  r19.43  2692  rabid2  2711  isset  2810  ralv  2821  rexv  2822  reuv  2823  rmov  2824  rexcom4b  2829  ceqsex4v  2848  ceqsex8v  2850  ceqsrexv  2937  ralrab2  2972  rexrab2  2974  reu2  2995  reu3  2997  reueq  3006  2reuswapdc  3011  reuind  3012  sbc3an  3094  rmo2ilem  3123  csbcow  3139  ssalel  3216  dfss3  3217  dfss3f  3220  ssabral  3299  rabss  3305  ssrabeq  3316  uniiunlem  3318  dfdif3  3319  ddifstab  3341  uncom  3353  inass  3419  indi  3456  difindiss  3463  difin2  3471  reupick3  3494  n0rf  3509  eq0  3515  eqv  3516  vss  3544  disj  3545  disj3  3549  undisj1  3554  undisj2  3555  exsnrex  3715  euabsn2  3744  euabsn  3745  snmb  3797  prssg  3835  dfuni2  3900  unissb  3928  elint2  3940  ssint  3949  dfiin2g  4008  iunn0m  4036  iunxun  4055  iunxiun  4057  iinpw  4066  disjnim  4083  dftr2  4194  dftr5  4195  dftr3  4196  dftr4  4197  vnex  4225  inuni  4250  snelpw  4310  sspwb  4314  opelopabsb  4360  eusv2  4560  orddif  4651  onintexmid  4677  zfregfr  4678  tfi  4686  opthprc  4783  elxp3  4786  xpiundir  4791  elvv  4794  brinxp2  4799  relsn  4837  reliun  4854  inxp  4870  raliunxp  4877  rexiunxp  4878  cnvuni  4922  dm0rn0  4954  elrn  4981  ssdmres  5041  dfres2  5071  dfima2  5084  args  5112  cotr  5125  intasym  5128  asymref  5129  intirr  5130  cnv0  5147  xp11m  5182  cnvresima  5233  resco  5248  rnco  5250  coiun  5253  coass  5262  dfiota2  5294  dffun2  5343  dffun6f  5346  dffun4f  5349  dffun7  5360  dffun9  5362  funfn  5363  svrelfun  5402  imadiflem  5416  dffn2  5491  dffn3  5500  fintm  5530  dffn4  5574  dff1o4  5600  brprcneu  5641  eqfnfv3  5755  fnreseql  5766  fsn  5827  abrexco  5910  imaiun  5911  mpo2eqb  6141  elovmpo  6231  abexex  6297  releldm2  6357  fnmpo  6376  cnvimadfsn  6423  dftpos4  6472  tfrlem7  6526  0er  6779  eroveu  6838  erovlem  6839  map0e  6898  elixpconst  6918  domen  6965  reuen1  7018  xpf1o  7073  ssfilem  7105  ssfilemd  7107  finexdc  7135  pw1dc0el  7146  ssfirab  7172  sbthlemi10  7208  djuexb  7286  sspw1or2  7446  iftrueb01  7484  pw1if  7486  dmaddpq  7642  dmmulpq  7643  distrnqg  7650  enq0enq  7694  enq0tr  7697  nqnq0pi  7701  distrnq0  7722  prltlu  7750  prarloc  7766  genpdflem  7770  ltexprlemm  7863  ltexprlemlol  7865  ltexprlemupu  7867  ltexprlemdisj  7869  recexprlemdisj  7893  ltresr  8102  elnnz  9533  dfz2  9596  2rexuz  9860  eluz2b1  9879  elxr  10055  elixx1  10176  elioo2  10200  elioopnf  10246  elicopnf  10248  elfz1  10293  fzdifsuc  10361  fznn  10369  fzp1nel  10384  fznn0  10393  dfrp2  10569  redivap  11497  imdivap  11504  rexanre  11843  climreu  11920  prodmodc  12202  3dvdsdec  12489  3dvds2dec  12490  bitsval  12567  bezoutlembi  12639  nnwosdc  12673  isprm2  12752  isprm3  12753  isprm4  12754  pythagtriplem2  12902  elgz  13007  inffinp1  13113  isnsg4  13862  isrng  14011  isring  14077  dfrhm2  14232  lss1d  14462  isbasis3g  14840  restsn  14974  lmbr  15007  txbas  15052  tx2cn  15064  elcncf1di  15373  dedekindicclemicc  15426  limcrcl  15452  isclwwlk  16318  clwwlkccatlem  16324  eupth2lem1  16382  bj-nnor  16435  bj-vprc  16595  ss1oel2o  16690  subctctexmid  16705  trirec0xor  16760