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  948  mpbiran2  949  3anrev  1014  an6  1357  nfand  1616  19.33b2  1677  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  2399  dcne  2413  necon3bii  2440  ne3anior  2490  r2alf  2549  r2exf  2550  r19.23t  2640  r19.26-3  2663  r19.26m  2664  r19.43  2691  rabid2  2710  isset  2809  ralv  2820  rexv  2821  reuv  2822  rmov  2823  rexcom4b  2828  ceqsex4v  2847  ceqsex8v  2849  ceqsrexv  2936  ralrab2  2971  rexrab2  2973  reu2  2994  reu3  2996  reueq  3005  2reuswapdc  3010  reuind  3011  sbc3an  3093  rmo2ilem  3122  csbcow  3138  ssalel  3215  dfss3  3216  dfss3f  3219  ssabral  3298  rabss  3304  ssrabeq  3314  uniiunlem  3316  dfdif3  3317  ddifstab  3339  uncom  3351  inass  3417  indi  3454  difindiss  3461  difin2  3469  reupick3  3492  n0rf  3507  eq0  3513  eqv  3514  vss  3542  disj  3543  disj3  3547  undisj1  3552  undisj2  3553  exsnrex  3711  euabsn2  3740  euabsn  3741  snmb  3793  prssg  3830  dfuni2  3895  unissb  3923  elint2  3935  ssint  3944  dfiin2g  4003  iunn0m  4031  iunxun  4050  iunxiun  4052  iinpw  4061  disjnim  4078  dftr2  4189  dftr5  4190  dftr3  4191  dftr4  4192  vnex  4220  inuni  4245  snelpw  4304  sspwb  4308  opelopabsb  4354  eusv2  4554  orddif  4645  onintexmid  4671  zfregfr  4672  tfi  4680  opthprc  4777  elxp3  4780  xpiundir  4785  elvv  4788  brinxp2  4793  relsn  4831  reliun  4848  inxp  4864  raliunxp  4871  rexiunxp  4872  cnvuni  4916  dm0rn0  4948  elrn  4975  ssdmres  5035  dfres2  5065  dfima2  5078  args  5105  cotr  5118  intasym  5121  asymref  5122  intirr  5123  cnv0  5140  xp11m  5175  cnvresima  5226  resco  5241  rnco  5243  coiun  5246  coass  5255  dfiota2  5287  dffun2  5336  dffun6f  5339  dffun4f  5342  dffun7  5353  dffun9  5355  funfn  5356  svrelfun  5395  imadiflem  5409  dffn2  5484  dffn3  5493  fintm  5522  dffn4  5565  dff1o4  5591  brprcneu  5632  eqfnfv3  5746  fnreseql  5757  fsn  5819  abrexco  5900  imaiun  5901  mpo2eqb  6131  elovmpo  6221  abexex  6288  releldm2  6348  fnmpo  6367  dftpos4  6429  tfrlem7  6483  0er  6736  eroveu  6795  erovlem  6796  map0e  6855  elixpconst  6875  domen  6922  reuen1  6975  xpf1o  7030  ssfilem  7062  ssfilemd  7064  finexdc  7092  pw1dc0el  7103  ssfirab  7129  sbthlemi10  7165  djuexb  7243  sspw1or2  7403  iftrueb01  7441  pw1if  7443  dmaddpq  7599  dmmulpq  7600  distrnqg  7607  enq0enq  7651  enq0tr  7654  nqnq0pi  7658  distrnq0  7679  prltlu  7707  prarloc  7723  genpdflem  7727  ltexprlemm  7820  ltexprlemlol  7822  ltexprlemupu  7824  ltexprlemdisj  7826  recexprlemdisj  7850  ltresr  8059  elnnz  9489  dfz2  9552  2rexuz  9816  eluz2b1  9835  elxr  10011  elixx1  10132  elioo2  10156  elioopnf  10202  elicopnf  10204  elfz1  10248  fzdifsuc  10316  fznn  10324  fzp1nel  10339  fznn0  10348  dfrp2  10524  redivap  11452  imdivap  11459  rexanre  11798  climreu  11875  prodmodc  12157  3dvdsdec  12444  3dvds2dec  12445  bitsval  12522  bezoutlembi  12594  nnwosdc  12628  isprm2  12707  isprm3  12708  isprm4  12709  pythagtriplem2  12857  elgz  12962  inffinp1  13068  isnsg4  13817  isrng  13966  isring  14032  dfrhm2  14187  lss1d  14416  isbasis3g  14789  restsn  14923  lmbr  14956  txbas  15001  tx2cn  15013  elcncf1di  15322  dedekindicclemicc  15375  limcrcl  15401  isclwwlk  16264  clwwlkccatlem  16270  eupth2lem1  16328  bj-nnor  16381  bj-vprc  16542  ss1oel2o  16637  subctctexmid  16652  trirec0xor  16700