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  943  mpbiran2  944  3anrev  991  an6  1334  nfand  1592  19.33b2  1653  nf3  1693  nf4dc  1694  nf4r  1695  equsalh  1750  sb6x  1803  sb5f  1828  sbidm  1875  sb5  1912  sbanv  1914  sborv  1915  sbhb  1969  sb3an  1987  sbel2x  2027  sbal1yz  2030  sbexyz  2032  eu2  2099  2eu4  2148  cleqh  2306  cleqf  2374  dcne  2388  necon3bii  2415  ne3anior  2465  r2alf  2524  r2exf  2525  r19.23t  2614  r19.26-3  2637  r19.26m  2638  r19.43  2665  rabid2  2684  isset  2780  ralv  2791  rexv  2792  reuv  2793  rmov  2794  rexcom4b  2799  ceqsex4v  2818  ceqsex8v  2820  ceqsrexv  2907  ralrab2  2942  rexrab2  2944  reu2  2965  reu3  2967  reueq  2976  2reuswapdc  2981  reuind  2982  sbc3an  3064  rmo2ilem  3092  csbcow  3108  ssalel  3185  dfss3  3186  dfss3f  3189  ssabral  3268  rabss  3274  ssrabeq  3284  uniiunlem  3286  dfdif3  3287  ddifstab  3309  uncom  3321  inass  3387  indi  3424  difindiss  3431  difin2  3439  reupick3  3462  n0rf  3477  eq0  3483  eqv  3484  vss  3512  disj  3513  disj3  3517  undisj1  3522  undisj2  3523  exsnrex  3680  euabsn2  3707  euabsn  3708  snmb  3759  prssg  3796  dfuni2  3858  unissb  3886  elint2  3898  ssint  3907  dfiin2g  3966  iunn0m  3994  iunxun  4013  iunxiun  4015  iinpw  4024  disjnim  4041  dftr2  4152  dftr5  4153  dftr3  4154  dftr4  4155  vnex  4183  inuni  4207  snelpw  4265  sspwb  4268  opelopabsb  4314  eusv2  4512  orddif  4603  onintexmid  4629  zfregfr  4630  tfi  4638  opthprc  4734  elxp3  4737  xpiundir  4742  elvv  4745  brinxp2  4750  relsn  4788  reliun  4804  inxp  4820  raliunxp  4827  rexiunxp  4828  cnvuni  4872  dm0rn0  4904  elrn  4930  ssdmres  4990  dfres2  5020  dfima2  5033  args  5060  cotr  5073  intasym  5076  asymref  5077  intirr  5078  cnv0  5095  xp11m  5130  cnvresima  5181  resco  5196  rnco  5198  coiun  5201  coass  5210  dfiota2  5242  dffun2  5290  dffun6f  5293  dffun4f  5296  dffun7  5307  dffun9  5309  funfn  5310  svrelfun  5348  imadiflem  5362  dffn2  5437  dffn3  5446  fintm  5473  dffn4  5516  dff1o4  5542  brprcneu  5582  eqfnfv3  5692  fnreseql  5703  fsn  5765  abrexco  5841  imaiun  5842  mpo2eqb  6068  elovmpo  6158  abexex  6224  releldm2  6284  fnmpo  6301  dftpos4  6362  tfrlem7  6416  0er  6667  eroveu  6726  erovlem  6727  map0e  6786  elixpconst  6806  domen  6853  reuen1  6906  xpf1o  6956  ssfilem  6987  finexdc  7014  pw1dc0el  7023  ssfirab  7048  sbthlemi10  7083  djuexb  7161  iftrueb01  7354  pw1if  7356  dmaddpq  7512  dmmulpq  7513  distrnqg  7520  enq0enq  7564  enq0tr  7567  nqnq0pi  7571  distrnq0  7592  prltlu  7620  prarloc  7636  genpdflem  7640  ltexprlemm  7733  ltexprlemlol  7735  ltexprlemupu  7737  ltexprlemdisj  7739  recexprlemdisj  7763  ltresr  7972  elnnz  9402  dfz2  9465  2rexuz  9723  eluz2b1  9742  elxr  9918  elixx1  10039  elioo2  10063  elioopnf  10109  elicopnf  10111  elfz1  10155  fzdifsuc  10223  fznn  10231  fzp1nel  10246  fznn0  10255  dfrp2  10428  redivap  11260  imdivap  11267  rexanre  11606  climreu  11683  prodmodc  11964  3dvdsdec  12251  3dvds2dec  12252  bitsval  12329  bezoutlembi  12401  nnwosdc  12435  isprm2  12514  isprm3  12515  isprm4  12516  pythagtriplem2  12664  elgz  12769  inffinp1  12875  isnsg4  13623  isrng  13771  isring  13837  dfrhm2  13991  lss1d  14220  isbasis3g  14593  restsn  14727  lmbr  14760  txbas  14805  tx2cn  14817  elcncf1di  15126  dedekindicclemicc  15179  limcrcl  15205  bj-nnor  15809  bj-vprc  15970  ss1oel2o  16066  subctctexmid  16078  trirec0xor  16125