Theorem bitr4i 186

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 131	. 2 |- ( ps <-> ch )
4	1, 3	bitri 183	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2i  207  3bitr2ri  208  3bitr4i  211  3bitr4ri  212  biancomi  268  imdistan  441  biadani  602  mpbiran  930  mpbiran2  931  3anrev  978  an6  1311  nfand  1556  19.33b2  1617  nf3  1657  nf4dc  1658  nf4r  1659  equsalh  1714  sb6x  1767  sb5f  1792  sbidm  1839  sb5  1875  sbanv  1877  sborv  1878  sbhb  1928  sb3an  1946  sbel2x  1986  sbal1yz  1989  sbexyz  1991  eu2  2058  2eu4  2107  cleqh  2265  cleqf  2332  dcne  2346  necon3bii  2373  ne3anior  2423  r2alf  2482  r2exf  2483  r19.23t  2572  r19.26-3  2595  r19.26m  2596  r19.43  2623  rabid2  2641  isset  2731  ralv  2742  rexv  2743  reuv  2744  rmov  2745  rexcom4b  2750  ceqsex4v  2768  ceqsex8v  2770  ceqsrexv  2855  ralrab2  2890  rexrab2  2892  reu2  2913  reu3  2915  reueq  2924  2reuswapdc  2929  reuind  2930  sbc3an  3011  rmo2ilem  3039  csbcow  3055  dfss2  3130  dfss3  3131  dfss3f  3133  ssabral  3212  rabss  3218  ssrabeq  3228  uniiunlem  3230  dfdif3  3231  ddifstab  3253  uncom  3265  inass  3331  indi  3368  difindiss  3375  difin2  3383  reupick3  3406  n0rf  3420  eq0  3426  eqv  3427  vss  3455  disj  3456  disj3  3460  undisj1  3465  undisj2  3466  exsnrex  3617  euabsn2  3644  euabsn  3645  prssg  3729  dfuni2  3790  unissb  3818  elint2  3830  ssint  3839  dfiin2g  3898  iunn0m  3925  iunxun  3944  iunxiun  3946  iinpw  3955  disjnim  3972  dftr2  4081  dftr5  4082  dftr3  4083  dftr4  4084  vnex  4112  inuni  4133  snelpw  4190  sspwb  4193  opelopabsb  4237  eusv2  4434  orddif  4523  onintexmid  4549  zfregfr  4550  tfi  4558  opthprc  4654  elxp3  4657  xpiundir  4662  elvv  4665  brinxp2  4670  relsn  4708  reliun  4724  inxp  4737  raliunxp  4744  rexiunxp  4745  cnvuni  4789  dm0rn0  4820  elrn  4846  ssdmres  4905  dfres2  4935  dfima2  4947  args  4972  cotr  4984  intasym  4987  asymref  4988  intirr  4989  cnv0  5006  xp11m  5041  cnvresima  5092  resco  5107  rnco  5109  coiun  5112  coass  5121  dfiota2  5153  dffun2  5197  dffun6f  5200  dffun4f  5203  dffun7  5214  dffun9  5216  funfn  5217  svrelfun  5252  imadiflem  5266  dffn2  5338  dffn3  5347  fintm  5372  dffn4  5415  dff1o4  5439  brprcneu  5478  eqfnfv3  5584  fnreseql  5594  fsn  5656  abrexco  5726  imaiun  5727  mpo2eqb  5947  elovmpo  6038  abexex  6091  releldm2  6150  fnmpo  6167  dftpos4  6227  tfrlem7  6281  0er  6531  eroveu  6588  erovlem  6589  map0e  6648  elixpconst  6668  domen  6713  reuen1  6763  xpf1o  6806  ssfilem  6837  finexdc  6864  pw1dc0el  6873  ssfirab  6895  sbthlemi10  6927  djuexb  7005  dmaddpq  7316  dmmulpq  7317  distrnqg  7324  enq0enq  7368  enq0tr  7371  nqnq0pi  7375  distrnq0  7396  prltlu  7424  prarloc  7440  genpdflem  7444  ltexprlemm  7537  ltexprlemlol  7539  ltexprlemupu  7541  ltexprlemdisj  7543  recexprlemdisj  7567  ltresr  7776  elnnz  9197  dfz2  9259  2rexuz  9516  eluz2b1  9535  elxr  9708  elixx1  9829  elioo2  9853  elioopnf  9899  elicopnf  9901  elfz1  9945  fzdifsuc  10012  fznn  10020  fzp1nel  10035  fznn0  10044  dfrp2  10195  redivap  10812  imdivap  10819  rexanre  11158  climreu  11234  prodmodc  11515  3dvdsdec  11798  3dvds2dec  11799  bezoutlembi  11934  nnwosdc  11968  isprm2  12045  isprm3  12046  isprm4  12047  pythagtriplem2  12194  elgz  12297  inffinp1  12358  isbasis3g  12644  restsn  12780  lmbr  12813  txbas  12858  tx2cn  12870  elcncf1di  13166  dedekindicclemicc  13210  limcrcl  13227  bj-nnor  13575  bj-vprc  13738  ss1oel2o  13833  subctctexmid  13841  trirec0xor  13884