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  612  mpbiran  942  mpbiran2  943  3anrev  990  an6  1332  nfand  1582  19.33b2  1643  nf3  1683  nf4dc  1684  nf4r  1685  equsalh  1740  sb6x  1793  sb5f  1818  sbidm  1865  sb5  1902  sbanv  1904  sborv  1905  sbhb  1959  sb3an  1977  sbel2x  2017  sbal1yz  2020  sbexyz  2022  eu2  2089  2eu4  2138  cleqh  2296  cleqf  2364  dcne  2378  necon3bii  2405  ne3anior  2455  r2alf  2514  r2exf  2515  r19.23t  2604  r19.26-3  2627  r19.26m  2628  r19.43  2655  rabid2  2674  isset  2769  ralv  2780  rexv  2781  reuv  2782  rmov  2783  rexcom4b  2788  ceqsex4v  2807  ceqsex8v  2809  ceqsrexv  2894  ralrab2  2929  rexrab2  2931  reu2  2952  reu3  2954  reueq  2963  2reuswapdc  2968  reuind  2969  sbc3an  3051  rmo2ilem  3079  csbcow  3095  dfss2  3172  dfss3  3173  dfss3f  3175  ssabral  3254  rabss  3260  ssrabeq  3270  uniiunlem  3272  dfdif3  3273  ddifstab  3295  uncom  3307  inass  3373  indi  3410  difindiss  3417  difin2  3425  reupick3  3448  n0rf  3463  eq0  3469  eqv  3470  vss  3498  disj  3499  disj3  3503  undisj1  3508  undisj2  3509  exsnrex  3664  euabsn2  3691  euabsn  3692  prssg  3779  dfuni2  3841  unissb  3869  elint2  3881  ssint  3890  dfiin2g  3949  iunn0m  3977  iunxun  3996  iunxiun  3998  iinpw  4007  disjnim  4024  dftr2  4133  dftr5  4134  dftr3  4135  dftr4  4136  vnex  4164  inuni  4188  snelpw  4246  sspwb  4249  opelopabsb  4294  eusv2  4492  orddif  4583  onintexmid  4609  zfregfr  4610  tfi  4618  opthprc  4714  elxp3  4717  xpiundir  4722  elvv  4725  brinxp2  4730  relsn  4768  reliun  4784  inxp  4800  raliunxp  4807  rexiunxp  4808  cnvuni  4852  dm0rn0  4883  elrn  4909  ssdmres  4968  dfres2  4998  dfima2  5011  args  5038  cotr  5051  intasym  5054  asymref  5055  intirr  5056  cnv0  5073  xp11m  5108  cnvresima  5159  resco  5174  rnco  5176  coiun  5179  coass  5188  dfiota2  5220  dffun2  5268  dffun6f  5271  dffun4f  5274  dffun7  5285  dffun9  5287  funfn  5288  svrelfun  5323  imadiflem  5337  dffn2  5409  dffn3  5418  fintm  5443  dffn4  5486  dff1o4  5512  brprcneu  5551  eqfnfv3  5661  fnreseql  5672  fsn  5734  abrexco  5806  imaiun  5807  mpo2eqb  6032  elovmpo  6122  abexex  6183  releldm2  6243  fnmpo  6260  dftpos4  6321  tfrlem7  6375  0er  6626  eroveu  6685  erovlem  6686  map0e  6745  elixpconst  6765  domen  6810  reuen1  6860  xpf1o  6905  ssfilem  6936  finexdc  6963  pw1dc0el  6972  ssfirab  6997  sbthlemi10  7032  djuexb  7110  dmaddpq  7446  dmmulpq  7447  distrnqg  7454  enq0enq  7498  enq0tr  7501  nqnq0pi  7505  distrnq0  7526  prltlu  7554  prarloc  7570  genpdflem  7574  ltexprlemm  7667  ltexprlemlol  7669  ltexprlemupu  7671  ltexprlemdisj  7673  recexprlemdisj  7697  ltresr  7906  elnnz  9336  dfz2  9398  2rexuz  9656  eluz2b1  9675  elxr  9851  elixx1  9972  elioo2  9996  elioopnf  10042  elicopnf  10044  elfz1  10088  fzdifsuc  10156  fznn  10164  fzp1nel  10179  fznn0  10188  dfrp2  10353  redivap  11039  imdivap  11046  rexanre  11385  climreu  11462  prodmodc  11743  3dvdsdec  12030  3dvds2dec  12031  bitsval  12108  bezoutlembi  12172  nnwosdc  12206  isprm2  12285  isprm3  12286  isprm4  12287  pythagtriplem2  12435  elgz  12540  inffinp1  12646  isnsg4  13342  isrng  13490  isring  13556  dfrhm2  13710  lss1d  13939  isbasis3g  14282  restsn  14416  lmbr  14449  txbas  14494  tx2cn  14506  elcncf1di  14815  dedekindicclemicc  14868  limcrcl  14894  bj-nnor  15380  bj-vprc  15542  ss1oel2o  15638  subctctexmid  15645  trirec0xor  15689