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  614  mpbiran  946  mpbiran2  947  3anrev  1012  an6  1355  nfand  1614  19.33b2  1675  nf3  1715  nf4dc  1716  nf4r  1717  equsalh  1772  sb6x  1825  sb5f  1850  sbidm  1897  sb5  1934  sbanv  1936  sborv  1937  sbhb  1991  sb3an  2009  sbel2x  2049  sbal1yz  2052  sbexyz  2054  eu2  2122  2eu4  2171  cleqh  2329  cleqf  2397  dcne  2411  necon3bii  2438  ne3anior  2488  r2alf  2547  r2exf  2548  r19.23t  2638  r19.26-3  2661  r19.26m  2662  r19.43  2689  rabid2  2708  isset  2806  ralv  2817  rexv  2818  reuv  2819  rmov  2820  rexcom4b  2825  ceqsex4v  2844  ceqsex8v  2846  ceqsrexv  2933  ralrab2  2968  rexrab2  2970  reu2  2991  reu3  2993  reueq  3002  2reuswapdc  3007  reuind  3008  sbc3an  3090  rmo2ilem  3119  csbcow  3135  ssalel  3212  dfss3  3213  dfss3f  3216  ssabral  3295  rabss  3301  ssrabeq  3311  uniiunlem  3313  dfdif3  3314  ddifstab  3336  uncom  3348  inass  3414  indi  3451  difindiss  3458  difin2  3466  reupick3  3489  n0rf  3504  eq0  3510  eqv  3511  vss  3539  disj  3540  disj3  3544  undisj1  3549  undisj2  3550  exsnrex  3708  euabsn2  3735  euabsn  3736  snmb  3788  prssg  3825  dfuni2  3890  unissb  3918  elint2  3930  ssint  3939  dfiin2g  3998  iunn0m  4026  iunxun  4045  iunxiun  4047  iinpw  4056  disjnim  4073  dftr2  4184  dftr5  4185  dftr3  4186  dftr4  4187  vnex  4215  inuni  4239  snelpw  4298  sspwb  4302  opelopabsb  4348  eusv2  4548  orddif  4639  onintexmid  4665  zfregfr  4666  tfi  4674  opthprc  4770  elxp3  4773  xpiundir  4778  elvv  4781  brinxp2  4786  relsn  4824  reliun  4840  inxp  4856  raliunxp  4863  rexiunxp  4864  cnvuni  4908  dm0rn0  4940  elrn  4967  ssdmres  5027  dfres2  5057  dfima2  5070  args  5097  cotr  5110  intasym  5113  asymref  5114  intirr  5115  cnv0  5132  xp11m  5167  cnvresima  5218  resco  5233  rnco  5235  coiun  5238  coass  5247  dfiota2  5279  dffun2  5328  dffun6f  5331  dffun4f  5334  dffun7  5345  dffun9  5347  funfn  5348  svrelfun  5386  imadiflem  5400  dffn2  5475  dffn3  5484  fintm  5513  dffn4  5556  dff1o4  5582  brprcneu  5622  eqfnfv3  5736  fnreseql  5747  fsn  5809  abrexco  5889  imaiun  5890  mpo2eqb  6120  elovmpo  6210  abexex  6277  releldm2  6337  fnmpo  6354  dftpos4  6415  tfrlem7  6469  0er  6722  eroveu  6781  erovlem  6782  map0e  6841  elixpconst  6861  domen  6908  reuen1  6961  xpf1o  7013  ssfilem  7045  finexdc  7073  pw1dc0el  7084  ssfirab  7109  sbthlemi10  7144  djuexb  7222  iftrueb01  7419  pw1if  7421  dmaddpq  7577  dmmulpq  7578  distrnqg  7585  enq0enq  7629  enq0tr  7632  nqnq0pi  7636  distrnq0  7657  prltlu  7685  prarloc  7701  genpdflem  7705  ltexprlemm  7798  ltexprlemlol  7800  ltexprlemupu  7802  ltexprlemdisj  7804  recexprlemdisj  7828  ltresr  8037  elnnz  9467  dfz2  9530  2rexuz  9789  eluz2b1  9808  elxr  9984  elixx1  10105  elioo2  10129  elioopnf  10175  elicopnf  10177  elfz1  10221  fzdifsuc  10289  fznn  10297  fzp1nel  10312  fznn0  10321  dfrp2  10495  redivap  11400  imdivap  11407  rexanre  11746  climreu  11823  prodmodc  12104  3dvdsdec  12391  3dvds2dec  12392  bitsval  12469  bezoutlembi  12541  nnwosdc  12575  isprm2  12654  isprm3  12655  isprm4  12656  pythagtriplem2  12804  elgz  12909  inffinp1  13015  isnsg4  13764  isrng  13912  isring  13978  dfrhm2  14133  lss1d  14362  isbasis3g  14735  restsn  14869  lmbr  14902  txbas  14947  tx2cn  14959  elcncf1di  15268  dedekindicclemicc  15321  limcrcl  15347  isclwwlk  16132  clwwlkccatlem  16137  bj-nnor  16153  bj-vprc  16314  ss1oel2o  16410  subctctexmid  16425  trirec0xor  16473