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  616  mpbiran  949  mpbiran2  950  3anrev  1015  an6  1358  nfand  1617  19.33b2  1678  nf3  1717  nf4dc  1718  nf4r  1719  equsalh  1774  sb6x  1828  sb5f  1853  sbidm  1900  sb5  1937  sbanv  1939  sborv  1940  sbhb  1994  sb3an  2012  sbel2x  2052  sbal1yz  2055  sbexyz  2057  eu2  2125  2eu4  2174  cleqh  2332  cleqf  2409  dcne  2423  necon3bii  2450  ne3anior  2500  r2alf  2559  r2exf  2560  r19.23t  2650  r19.26-3  2673  r19.26m  2674  r19.43  2701  rabid2  2721  isset  2820  ralv  2831  rexv  2832  reuv  2833  rmov  2834  rexcom4b  2839  ceqsex4v  2858  ceqsex8v  2860  ceqsrexv  2947  ralrab2  2982  rexrab2  2984  reu2  3005  reu3  3007  reueq  3016  2reuswapdc  3021  reuind  3022  sbc3an  3104  rmo2ilem  3133  csbcow  3149  ssalel  3226  dfss3  3227  dfss3f  3230  ssabral  3309  rabss  3315  ssrabeq  3326  uniiunlem  3328  dfdif3  3329  ddifstab  3351  uncom  3363  inass  3431  indi  3468  difindiss  3475  difin2  3483  reupick3  3506  n0rf  3521  eq0  3527  eqv  3528  vss  3556  disj  3557  disj3  3561  undisj1  3566  undisj2  3567  exsnrex  3731  euabsn2  3760  euabsn  3761  snmb  3813  prssg  3851  dfuni2  3916  unissb  3944  elint2  3956  ssint  3965  dfiin2g  4024  iunn0m  4052  iunxun  4071  iunxiun  4073  iinpw  4082  disjnim  4099  dftr2  4210  dftr5  4211  dftr3  4212  dftr4  4213  vnex  4241  inuni  4267  snelpw  4328  sspwb  4332  opelopabsb  4378  eusv2  4578  orddif  4669  onintexmid  4695  zfregfr  4696  tfi  4704  opthprc  4801  elxp3  4804  xpiundir  4809  elvv  4812  brinxp2  4817  relsn  4855  reliun  4873  inxp  4889  raliunxp  4896  rexiunxp  4897  cnvuni  4941  dm0rn0  4973  elrn  5000  ssdmres  5060  dfres2  5090  dfima2  5103  args  5131  cotr  5144  intasym  5147  asymref  5148  intirr  5149  cnv0  5166  xp11m  5201  cnvresima  5252  resco  5267  rnco  5269  coiun  5272  coass  5281  dfiota2  5313  dffun2  5362  dffun6f  5365  dffun4f  5368  dffun7  5379  dffun9  5381  funfn  5382  svrelfun  5421  imadiflem  5435  dffn2  5510  dffn3  5519  fintm  5552  dffn4  5596  dff1o4  5622  brprcneu  5663  eqfnfv3  5777  fnreseql  5788  fsn  5849  abrexco  5932  imaiun  5933  mpo2eqb  6163  elovmpo  6253  abexex  6319  releldm2  6379  fnmpo  6398  cnvimadfsn  6445  dftpos4  6494  tfrlem7  6548  0er  6801  eroveu  6860  erovlem  6861  map0e  6920  elixpconst  6941  domen  6988  reuen1  7041  xpf1o  7097  ssfilem  7130  ssfilemd  7132  finexdc  7160  pw1dc0el  7171  ssfirab  7197  sbthlemi10  7236  djuexb  7335  sspw1or2  7495  iftrueb01  7533  pw1if  7535  dmaddpq  7694  dmmulpq  7695  distrnqg  7702  enq0enq  7746  enq0tr  7749  nqnq0pi  7753  distrnq0  7774  prltlu  7802  prarloc  7818  genpdflem  7822  ltexprlemm  7915  ltexprlemlol  7917  ltexprlemupu  7919  ltexprlemdisj  7921  recexprlemdisj  7945  ltresr  8154  elnnz  9587  dfz2  9650  2rexuz  9914  eluz2b1  9933  elxr  10109  elixx1  10230  elioo2  10254  elioopnf  10300  elicopnf  10302  elfz1  10347  fzdifsuc  10415  fznn  10423  fzp1nel  10438  fznn0  10447  dfrp2  10623  redivap  11559  imdivap  11566  rexanre  11905  climreu  11982  prodmodc  12264  3dvdsdec  12551  3dvds2dec  12552  bitsval  12629  bezoutlembi  12701  nnwosdc  12735  isprm2  12814  isprm3  12815  isprm4  12816  pythagtriplem2  12964  elgz  13069  inffinp1  13180  isnsg4  13929  isrng  14078  isring  14144  dfrhm2  14299  lss1d  14531  isbasis3g  14911  restsn  15045  lmbr  15078  txbas  15123  tx2cn  15135  elcncf1di  15444  dedekindicclemicc  15497  limcrcl  15523  isclwwlk  16389  clwwlkccatlem  16395  eupth2lem1  16453  bj-nnor  16506  bj-vprc  16666  ss1oel2o  16761  subctctexmid  16774  trirec0xor  16829