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  925  mpbiran2  926  3anrev  973  an6  1300  nfand  1548  19.33b2  1609  nf3  1648  nf4dc  1649  nf4r  1650  equsalh  1705  sb6x  1753  sb5f  1777  sbidm  1824  sb5  1860  sbanv  1862  sborv  1863  sbhb  1914  sb3an  1932  sbel2x  1974  sbal1yz  1977  sbexyz  1979  eu2  2044  2eu4  2093  cleqh  2240  cleqf  2306  dcne  2320  necon3bii  2347  ne3anior  2397  r2alf  2455  r2exf  2456  r19.23t  2542  r19.26-3  2565  r19.26m  2566  r19.43  2592  rabid2  2610  isset  2695  ralv  2706  rexv  2707  reuv  2708  rmov  2709  rexcom4b  2714  ceqsex4v  2732  ceqsex8v  2734  ceqsrexv  2819  ralrab2  2853  rexrab2  2855  reu2  2876  reu3  2878  reueq  2887  2reuswapdc  2892  reuind  2893  sbc3an  2974  rmo2ilem  3002  dfss2  3091  dfss3  3092  dfss3f  3094  ssabral  3173  rabss  3179  ssrabeq  3188  uniiunlem  3190  dfdif3  3191  ddifstab  3213  uncom  3225  inass  3291  indi  3328  difindiss  3335  difin2  3343  reupick3  3366  n0rf  3380  eq0  3386  eqv  3387  vss  3415  disj  3416  disj3  3420  undisj1  3425  undisj2  3426  exsnrex  3573  euabsn2  3600  euabsn  3601  prssg  3685  dfuni2  3746  unissb  3774  elint2  3786  ssint  3795  dfiin2g  3854  iunn0m  3881  iunxun  3900  iunxiun  3902  iinpw  3911  disjnim  3928  dftr2  4036  dftr5  4037  dftr3  4038  dftr4  4039  vnex  4067  inuni  4088  snelpw  4143  sspwb  4146  opelopabsb  4190  eusv2  4386  orddif  4470  onintexmid  4495  zfregfr  4496  tfi  4504  opthprc  4598  elxp3  4601  xpiundir  4606  elvv  4609  brinxp2  4614  relsn  4652  reliun  4668  inxp  4681  raliunxp  4688  rexiunxp  4689  cnvuni  4733  dm0rn0  4764  elrn  4790  ssdmres  4849  dfres2  4879  dfima2  4891  args  4916  cotr  4928  intasym  4931  asymref  4932  intirr  4933  cnv0  4950  xp11m  4985  cnvresima  5036  resco  5051  rnco  5053  coiun  5056  coass  5065  dfiota2  5097  dffun2  5141  dffun6f  5144  dffun4f  5147  dffun7  5158  dffun9  5160  funfn  5161  svrelfun  5196  imadiflem  5210  dffn2  5282  dffn3  5291  fintm  5316  dffn4  5359  dff1o4  5383  brprcneu  5422  eqfnfv3  5528  fnreseql  5538  fsn  5600  abrexco  5668  imaiun  5669  mpo2eqb  5888  elovmpo  5979  abexex  6032  releldm2  6091  fnmpo  6108  dftpos4  6168  tfrlem7  6222  0er  6471  eroveu  6528  erovlem  6529  map0e  6588  elixpconst  6608  domen  6653  reuen1  6703  xpf1o  6746  ssfilem  6777  finexdc  6804  ssfirab  6830  sbthlemi10  6862  djuexb  6937  dmaddpq  7211  dmmulpq  7212  distrnqg  7219  enq0enq  7263  enq0tr  7266  nqnq0pi  7270  distrnq0  7291  prltlu  7319  prarloc  7335  genpdflem  7339  ltexprlemm  7432  ltexprlemlol  7434  ltexprlemupu  7436  ltexprlemdisj  7438  recexprlemdisj  7462  ltresr  7671  elnnz  9088  dfz2  9147  2rexuz  9404  eluz2b1  9422  elxr  9593  elixx1  9710  elioo2  9734  elioopnf  9780  elicopnf  9782  elfz1  9826  fzdifsuc  9892  fznn  9900  fzp1nel  9915  fznn0  9924  redivap  10678  imdivap  10685  rexanre  11024  climreu  11098  prodmodc  11379  3dvdsdec  11598  3dvds2dec  11599  bezoutlembi  11729  isprm2  11834  isprm3  11835  isprm4  11836  inffinp1  11978  isbasis3g  12252  restsn  12388  lmbr  12421  txbas  12466  tx2cn  12478  elcncf1di  12774  dedekindicclemicc  12818  limcrcl  12835  bj-nnor  13117  bj-vprc  13265  ss1oel2o  13360  subctctexmid  13369  trirec0xor  13413