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  3787  prssg  3824  dfuni2  3889  unissb  3917  elint2  3929  ssint  3938  dfiin2g  3997  iunn0m  4025  iunxun  4044  iunxiun  4046  iinpw  4055  disjnim  4072  dftr2  4183  dftr5  4184  dftr3  4185  dftr4  4186  vnex  4214  inuni  4238  snelpw  4297  sspwb  4301  opelopabsb  4347  eusv2  4547  orddif  4638  onintexmid  4664  zfregfr  4665  tfi  4673  opthprc  4769  elxp3  4772  xpiundir  4777  elvv  4780  brinxp2  4785  relsn  4823  reliun  4839  inxp  4855  raliunxp  4862  rexiunxp  4863  cnvuni  4907  dm0rn0  4939  elrn  4966  ssdmres  5026  dfres2  5056  dfima2  5069  args  5096  cotr  5109  intasym  5112  asymref  5113  intirr  5114  cnv0  5131  xp11m  5166  cnvresima  5217  resco  5232  rnco  5234  coiun  5237  coass  5246  dfiota2  5278  dffun2  5327  dffun6f  5330  dffun4f  5333  dffun7  5344  dffun9  5346  funfn  5347  svrelfun  5385  imadiflem  5399  dffn2  5474  dffn3  5483  fintm  5510  dffn4  5553  dff1o4  5579  brprcneu  5619  eqfnfv3  5733  fnreseql  5744  fsn  5806  abrexco  5882  imaiun  5883  mpo2eqb  6113  elovmpo  6203  abexex  6269  releldm2  6329  fnmpo  6346  dftpos4  6407  tfrlem7  6461  0er  6712  eroveu  6771  erovlem  6772  map0e  6831  elixpconst  6851  domen  6898  reuen1  6951  xpf1o  7001  ssfilem  7033  finexdc  7060  pw1dc0el  7069  ssfirab  7094  sbthlemi10  7129  djuexb  7207  iftrueb01  7404  pw1if  7406  dmaddpq  7562  dmmulpq  7563  distrnqg  7570  enq0enq  7614  enq0tr  7617  nqnq0pi  7621  distrnq0  7642  prltlu  7670  prarloc  7686  genpdflem  7690  ltexprlemm  7783  ltexprlemlol  7785  ltexprlemupu  7787  ltexprlemdisj  7789  recexprlemdisj  7813  ltresr  8022  elnnz  9452  dfz2  9515  2rexuz  9773  eluz2b1  9792  elxr  9968  elixx1  10089  elioo2  10113  elioopnf  10159  elicopnf  10161  elfz1  10205  fzdifsuc  10273  fznn  10281  fzp1nel  10296  fznn0  10305  dfrp2  10478  redivap  11380  imdivap  11387  rexanre  11726  climreu  11803  prodmodc  12084  3dvdsdec  12371  3dvds2dec  12372  bitsval  12449  bezoutlembi  12521  nnwosdc  12555  isprm2  12634  isprm3  12635  isprm4  12636  pythagtriplem2  12784  elgz  12889  inffinp1  12995  isnsg4  13744  isrng  13892  isring  13958  dfrhm2  14112  lss1d  14341  isbasis3g  14714  restsn  14848  lmbr  14881  txbas  14926  tx2cn  14938  elcncf1di  15247  dedekindicclemicc  15300  limcrcl  15326  bj-nnor  16056  bj-vprc  16217  ss1oel2o  16313  subctctexmid  16325  trirec0xor  16372