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  612  mpbiran  942  mpbiran2  943  3anrev  990  an6  1332  nfand  1582  19.33b2  1643  nf3  1683  nf4dc  1684  nf4r  1685  equsalh  1740  sb6x  1793  sb5f  1818  sbidm  1865  sb5  1902  sbanv  1904  sborv  1905  sbhb  1959  sb3an  1977  sbel2x  2017  sbal1yz  2020  sbexyz  2022  eu2  2089  2eu4  2138  cleqh  2296  cleqf  2364  dcne  2378  necon3bii  2405  ne3anior  2455  r2alf  2514  r2exf  2515  r19.23t  2604  r19.26-3  2627  r19.26m  2628  r19.43  2655  rabid2  2674  isset  2769  ralv  2780  rexv  2781  reuv  2782  rmov  2783  rexcom4b  2788  ceqsex4v  2807  ceqsex8v  2809  ceqsrexv  2894  ralrab2  2929  rexrab2  2931  reu2  2952  reu3  2954  reueq  2963  2reuswapdc  2968  reuind  2969  sbc3an  3051  rmo2ilem  3079  csbcow  3095  ssalel  3172  dfss3  3173  dfss3f  3176  ssabral  3255  rabss  3261  ssrabeq  3271  uniiunlem  3273  dfdif3  3274  ddifstab  3296  uncom  3308  inass  3374  indi  3411  difindiss  3418  difin2  3426  reupick3  3449  n0rf  3464  eq0  3470  eqv  3471  vss  3499  disj  3500  disj3  3504  undisj1  3509  undisj2  3510  exsnrex  3665  euabsn2  3692  euabsn  3693  prssg  3780  dfuni2  3842  unissb  3870  elint2  3882  ssint  3891  dfiin2g  3950  iunn0m  3978  iunxun  3997  iunxiun  3999  iinpw  4008  disjnim  4025  dftr2  4134  dftr5  4135  dftr3  4136  dftr4  4137  vnex  4165  inuni  4189  snelpw  4247  sspwb  4250  opelopabsb  4295  eusv2  4493  orddif  4584  onintexmid  4610  zfregfr  4611  tfi  4619  opthprc  4715  elxp3  4718  xpiundir  4723  elvv  4726  brinxp2  4731  relsn  4769  reliun  4785  inxp  4801  raliunxp  4808  rexiunxp  4809  cnvuni  4853  dm0rn0  4884  elrn  4910  ssdmres  4969  dfres2  4999  dfima2  5012  args  5039  cotr  5052  intasym  5055  asymref  5056  intirr  5057  cnv0  5074  xp11m  5109  cnvresima  5160  resco  5175  rnco  5177  coiun  5180  coass  5189  dfiota2  5221  dffun2  5269  dffun6f  5272  dffun4f  5275  dffun7  5286  dffun9  5288  funfn  5289  svrelfun  5324  imadiflem  5338  dffn2  5410  dffn3  5419  fintm  5444  dffn4  5487  dff1o4  5513  brprcneu  5552  eqfnfv3  5662  fnreseql  5673  fsn  5735  abrexco  5807  imaiun  5808  mpo2eqb  6034  elovmpo  6124  abexex  6185  releldm2  6245  fnmpo  6262  dftpos4  6323  tfrlem7  6377  0er  6628  eroveu  6687  erovlem  6688  map0e  6747  elixpconst  6767  domen  6812  reuen1  6862  xpf1o  6907  ssfilem  6938  finexdc  6965  pw1dc0el  6974  ssfirab  6999  sbthlemi10  7034  djuexb  7112  dmaddpq  7449  dmmulpq  7450  distrnqg  7457  enq0enq  7501  enq0tr  7504  nqnq0pi  7508  distrnq0  7529  prltlu  7557  prarloc  7573  genpdflem  7577  ltexprlemm  7670  ltexprlemlol  7672  ltexprlemupu  7674  ltexprlemdisj  7676  recexprlemdisj  7700  ltresr  7909  elnnz  9339  dfz2  9401  2rexuz  9659  eluz2b1  9678  elxr  9854  elixx1  9975  elioo2  9999  elioopnf  10045  elicopnf  10047  elfz1  10091  fzdifsuc  10159  fznn  10167  fzp1nel  10182  fznn0  10191  dfrp2  10356  redivap  11042  imdivap  11049  rexanre  11388  climreu  11465  prodmodc  11746  3dvdsdec  12033  3dvds2dec  12034  bitsval  12111  bezoutlembi  12183  nnwosdc  12217  isprm2  12296  isprm3  12297  isprm4  12298  pythagtriplem2  12446  elgz  12551  inffinp1  12657  isnsg4  13368  isrng  13516  isring  13582  dfrhm2  13736  lss1d  13965  isbasis3g  14308  restsn  14442  lmbr  14475  txbas  14520  tx2cn  14532  elcncf1di  14841  dedekindicclemicc  14894  limcrcl  14920  bj-nnor  15406  bj-vprc  15568  ss1oel2o  15664  subctctexmid  15673  trirec0xor  15718