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  6538  tfrlem7  6592  0er  6845  eroveu  6904  erovlem  6905  map0e  6971  elixpconst  6992  domen  7039  reuen1  7092  xpf1o  7148  ssfilem  7181  ssfilemd  7183  finexdc  7211  pw1dc0el  7222  ssfirab  7248  sbthlemi10  7288  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  9665  dfz2  9728  2rexuz  9998  eluz2b1  10017  elxr  10195  elixx1  10316  elioo2  10340  elioopnf  10386  elicopnf  10388  elfz1  10433  fzdifsuc  10505  fznn  10513  fzp1nel  10528  fznn0  10537  dfrp2  10715  hashf1  11309  redivap  11661  imdivap  11668  rexanre  12009  climreu  12088  prodmodc  12370  3dvdsdec  12657  3dvds2dec  12658  bitsval  12735  bezoutlembi  12807  nnwosdc  12841  isprm2  12920  isprm3  12921  isprm4  12922  pythagtriplem2  13074  elgz  13179  inffinp1  13378  isnsg4  14074  isrng  14340  isring  14411  dfrhm2  14570  lss1d  14829  isbasis3g  15272  restsn  15406  lmbr  15439  txbas  15484  tx2cn  15496  elcncf1di  15805  dedekindicclemicc  15858  limcrcl  15884  isclwwlk  16840  clwwlkccatlem  16846  eupth2lem1  16904  bj-nnor  16967  bj-vprc  17127  ss1oel2o  17222  subctctexmid  17235  trirec0xor  17301  dfrals2  17337  dfralseu2  17371