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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr2i  208  3bitr2ri  209  3bitr4i  212  3bitr4ri  213  biancomi  270  imdistan  448  bianass  473  biadani  620  mpbiran  953  mpbiran2  954  3anrev  1019  an6  1362  nfand  1621  19.33b2  1682  nf3  1721  nf4dc  1722  nf4r  1723  equsalh  1778  sb6x  1832  sb5f  1857  sbidm  1904  equsv  1938  sb5  1942  sbanv  1944  sborv  1945  sbhb  2000  sb3an  2018  sbel2x  2058  sbal1yz  2061  sbexyz  2063  eu2  2131  2eu4  2180  cleqh  2338  cleqf  2417  dcne  2431  necon3bii  2458  ne3anior  2508  r2alf  2567  r2exf  2568  r19.23t  2658  r19.26-3  2681  r19.26m  2682  r19.43  2709  rabid2  2729  isset  2828  ralv  2839  rexv  2840  reuv  2841  rmov  2842  rexcom4b  2847  ceqsex4v  2866  ceqsex8v  2868  ceqsrexv  2956  ralrab2  2991  rexrab2  2993  reu2  3014  reu3  3016  reueq  3025  2reuswapdc  3030  reuind  3031  sbc3an  3113  rmo2ilem  3142  csbcow  3158  ssalel  3235  dfss3  3236  dfss3f  3240  ssabral  3319  rabss  3325  ssrabeq  3336  uniiunlem  3338  dfdif3  3339  ddifstab  3361  uncom  3373  inass  3441  indi  3478  difindiss  3485  difin2  3493  reupick3  3518  n0rf  3534  eq0  3540  eqv  3541  vss  3568  disj  3573  disj3  3577  undisj1  3582  undisj2  3583  exsnrex  3751  euabsn2  3780  euabsn  3781  snmb  3834  prssg  3872  dfuni2  3937  unissb  3965  elint2  3977  ssint  3986  dfiin2g  4045  iunn0m  4073  iunxun  4092  iunxiun  4094  iinpw  4103  disjnim  4120  dftr2  4233  dftr5  4234  dftr3  4235  dftr4  4236  vnex  4266  inuni  4293  snelpw  4354  sspwb  4358  opelopabsb  4404  eusv2  4605  orddif  4696  onintexmid  4722  zfregfr  4723  tfi  4731  opthprc  4828  elxp3  4831  xpiundir  4836  elvv  4839  brinxp2  4844  relsn  4882  reliun  4900  inxp  4916  raliunxp  4923  rexiunxp  4924  cnvuni  4968  dm0rn0  5000  elrn  5027  ssdmres  5087  dfres2  5118  dfima2  5131  args  5159  cotr  5172  intasym  5175  asymref  5176  intirr  5177  cnv0  5194  xp11m  5229  cnvresima  5280  resco  5295  rnco  5297  coiun  5300  coass  5309  dfiota2  5341  dffun2  5390  dffun6f  5393  dffun4f  5396  dffun7  5407  dffun9  5409  funfn  5410  svrelfun  5449  imadiflem  5463  dffn2  5538  dffn3  5547  fintm  5580  dffn4  5624  dff1o4  5650  brprcneu  5691  eqfnfv3  5811  fnreseql  5822  fsn  5883  abrexco  5968  imaiun  5969  mpo2eqb  6201  elovmpo  6291  abexex  6359  releldm2  6423  fnmpo  6442  cnvimadfsn  6489  dftpos4  6539  tfrlem7  6593  0er  6846  eroveu  6905  erovlem  6906  map0e  6972  elixpconst  6994  domen  7041  reuen1  7094  xpf1o  7150  ssfilem  7183  ssfilemd  7185  finexdc  7213  pw1dc0el  7224  ssfirab  7250  sbthlemi10  7290  djuexb  7390  sspw1or2  7550  iftrueb01  7588  pw1if  7590  dmaddpq  7752  dmmulpq  7753  distrnqg  7760  enq0enq  7804  enq0tr  7807  nqnq0pi  7811  distrnq0  7832  prltlu  7860  prarloc  7876  genpdflem  7880  ltexprlemm  7973  ltexprlemlol  7975  ltexprlemupu  7977  ltexprlemdisj  7979  recexprlemdisj  8003  ltresr  8212  elnnz  9663  dfz2  9726  2rexuz  9997  eluz2b1  10016  elxr  10194  elixx1  10315  elioo2  10339  elioopnf  10385  elicopnf  10387  elfz1  10432  fzdifsuc  10504  fznn  10512  fzp1nel  10527  fznn0  10536  dfrp2  10714  hashf1  11308  redivap  11660  imdivap  11667  rexanre  12008  climreu  12087  prodmodc  12369  3dvdsdec  12656  3dvds2dec  12657  bitsval  12734  bezoutlembi  12806  nnwosdc  12840  isprm2  12919  isprm3  12920  isprm4  12921  pythagtriplem2  13073  elgz  13178  inffinp1  13377  isnsg4  14073  isrng  14339  isring  14410  dfrhm2  14569  lss1d  14828  isbasis3g  15289  restsn  15423  lmbr  15456  txbas  15501  tx2cn  15513  elcncf1di  15822  dedekindicclemicc  15875  limcrcl  15901  isclwwlk  16857  clwwlkccatlem  16863  eupth2lem1  16921  bj-nnor  16984  bj-vprc  17144  ss1oel2o  17239  subctctexmid  17252  trirec0xor  17318  dfrals2  17354  dfralseu2  17388