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  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  3567  disj  3572  disj3  3576  undisj1  3581  undisj2  3582  exsnrex  3747  euabsn2  3776  euabsn  3777  snmb  3829  prssg  3867  dfuni2  3932  unissb  3960  elint2  3972  ssint  3981  dfiin2g  4040  iunn0m  4068  iunxun  4087  iunxiun  4089  iinpw  4098  disjnim  4115  dftr2  4226  dftr5  4227  dftr3  4228  dftr4  4229  vnex  4259  inuni  4286  snelpw  4347  sspwb  4351  opelopabsb  4397  eusv2  4598  orddif  4689  onintexmid  4715  zfregfr  4716  tfi  4724  opthprc  4821  elxp3  4824  xpiundir  4829  elvv  4832  brinxp2  4837  relsn  4875  reliun  4893  inxp  4909  raliunxp  4916  rexiunxp  4917  cnvuni  4961  dm0rn0  4993  elrn  5020  ssdmres  5080  dfres2  5110  dfima2  5123  args  5151  cotr  5164  intasym  5167  asymref  5168  intirr  5169  cnv0  5186  xp11m  5221  cnvresima  5272  resco  5287  rnco  5289  coiun  5292  coass  5301  dfiota2  5333  dffun2  5382  dffun6f  5385  dffun4f  5388  dffun7  5399  dffun9  5401  funfn  5402  svrelfun  5441  imadiflem  5455  dffn2  5530  dffn3  5539  fintm  5572  dffn4  5616  dff1o4  5642  brprcneu  5683  eqfnfv3  5799  fnreseql  5810  fsn  5871  abrexco  5955  imaiun  5956  mpo2eqb  6188  elovmpo  6278  abexex  6345  releldm2  6409  fnmpo  6428  cnvimadfsn  6475  dftpos4  6524  tfrlem7  6578  0er  6831  eroveu  6890  erovlem  6891  map0e  6957  elixpconst  6978  domen  7025  reuen1  7078  xpf1o  7134  ssfilem  7167  ssfilemd  7169  finexdc  7197  pw1dc0el  7208  ssfirab  7234  sbthlemi10  7273  djuexb  7374  sspw1or2  7534  iftrueb01  7572  pw1if  7574  dmaddpq  7736  dmmulpq  7737  distrnqg  7744  enq0enq  7788  enq0tr  7791  nqnq0pi  7795  distrnq0  7816  prltlu  7844  prarloc  7860  genpdflem  7864  ltexprlemm  7957  ltexprlemlol  7959  ltexprlemupu  7961  ltexprlemdisj  7963  recexprlemdisj  7987  ltresr  8196  elnnz  9633  dfz2  9696  2rexuz  9961  eluz2b1  9980  elxr  10157  elixx1  10278  elioo2  10302  elioopnf  10348  elicopnf  10350  elfz1  10395  fzdifsuc  10466  fznn  10474  fzp1nel  10489  fznn0  10498  dfrp2  10676  hashf1  11265  redivap  11617  imdivap  11624  rexanre  11964  climreu  12041  prodmodc  12323  3dvdsdec  12610  3dvds2dec  12611  bitsval  12688  bezoutlembi  12760  nnwosdc  12794  isprm2  12873  isprm3  12874  isprm4  12875  pythagtriplem2  13023  elgz  13128  inffinp1  13298  isnsg4  13992  isrng  14208  isring  14278  dfrhm2  14434  lss1d  14692  isbasis3g  15070  restsn  15204  lmbr  15237  txbas  15282  tx2cn  15294  elcncf1di  15603  dedekindicclemicc  15656  limcrcl  15682  isclwwlk  16549  clwwlkccatlem  16555  eupth2lem1  16613  bj-nnor  16676  bj-vprc  16836  ss1oel2o  16931  subctctexmid  16944  trirec0xor  16999