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  4231  dftr5  4232  dftr3  4233  dftr4  4234  vnex  4264  inuni  4291  snelpw  4352  sspwb  4356  opelopabsb  4402  eusv2  4603  orddif  4694  onintexmid  4720  zfregfr  4721  tfi  4729  opthprc  4826  elxp3  4829  xpiundir  4834  elvv  4837  brinxp2  4842  relsn  4880  reliun  4898  inxp  4914  raliunxp  4921  rexiunxp  4922  cnvuni  4966  dm0rn0  4998  elrn  5025  ssdmres  5085  dfres2  5115  dfima2  5128  args  5156  cotr  5169  intasym  5172  asymref  5173  intirr  5174  cnv0  5191  xp11m  5226  cnvresima  5277  resco  5292  rnco  5294  coiun  5297  coass  5306  dfiota2  5338  dffun2  5387  dffun6f  5390  dffun4f  5393  dffun7  5404  dffun9  5406  funfn  5407  svrelfun  5446  imadiflem  5460  dffn2  5535  dffn3  5544  fintm  5577  dffn4  5621  dff1o4  5647  brprcneu  5688  eqfnfv3  5808  fnreseql  5819  fsn  5880  abrexco  5965  imaiun  5966  mpo2eqb  6198  elovmpo  6288  abexex  6355  releldm2  6419  fnmpo  6438  cnvimadfsn  6485  dftpos4  6534  tfrlem7  6588  0er  6841  eroveu  6900  erovlem  6901  map0e  6967  elixpconst  6988  domen  7035  reuen1  7088  xpf1o  7144  ssfilem  7177  ssfilemd  7179  finexdc  7207  pw1dc0el  7218  ssfirab  7244  sbthlemi10  7283  djuexb  7385  sspw1or2  7545  iftrueb01  7583  pw1if  7585  dmaddpq  7747  dmmulpq  7748  distrnqg  7755  enq0enq  7799  enq0tr  7802  nqnq0pi  7806  distrnq0  7827  prltlu  7855  prarloc  7871  genpdflem  7875  ltexprlemm  7968  ltexprlemlol  7970  ltexprlemupu  7972  ltexprlemdisj  7974  recexprlemdisj  7998  ltresr  8207  elnnz  9659  dfz2  9722  2rexuz  9992  eluz2b1  10011  elxr  10189  elixx1  10310  elioo2  10334  elioopnf  10380  elicopnf  10382  elfz1  10427  fzdifsuc  10499  fznn  10507  fzp1nel  10522  fznn0  10531  dfrp2  10709  hashf1  11303  redivap  11655  imdivap  11662  rexanre  12003  climreu  12082  prodmodc  12364  3dvdsdec  12651  3dvds2dec  12652  bitsval  12729  bezoutlembi  12801  nnwosdc  12835  isprm2  12914  isprm3  12915  isprm4  12916  pythagtriplem2  13068  elgz  13173  inffinp1  13372  isnsg4  14068  isrng  14317  isring  14388  dfrhm2  14545  lss1d  14804  isbasis3g  15238  restsn  15372  lmbr  15405  txbas  15450  tx2cn  15462  elcncf1di  15771  dedekindicclemicc  15824  limcrcl  15850  isclwwlk  16801  clwwlkccatlem  16807  eupth2lem1  16865  bj-nnor  16928  bj-vprc  17088  ss1oel2o  17183  subctctexmid  17196  trirec0xor  17261  dfrals2  17297  dfralseu2  17331