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  940  mpbiran2  941  3anrev  988  an6  1321  nfand  1568  19.33b2  1629  nf3  1669  nf4dc  1670  nf4r  1671  equsalh  1726  sb6x  1779  sb5f  1804  sbidm  1851  sb5  1887  sbanv  1889  sborv  1890  sbhb  1940  sb3an  1958  sbel2x  1998  sbal1yz  2001  sbexyz  2003  eu2  2070  2eu4  2119  cleqh  2277  cleqf  2344  dcne  2358  necon3bii  2385  ne3anior  2435  r2alf  2494  r2exf  2495  r19.23t  2584  r19.26-3  2607  r19.26m  2608  r19.43  2635  rabid2  2654  isset  2744  ralv  2755  rexv  2756  reuv  2757  rmov  2758  rexcom4b  2763  ceqsex4v  2781  ceqsex8v  2783  ceqsrexv  2868  ralrab2  2903  rexrab2  2905  reu2  2926  reu3  2928  reueq  2937  2reuswapdc  2942  reuind  2943  sbc3an  3025  rmo2ilem  3053  csbcow  3069  dfss2  3145  dfss3  3146  dfss3f  3148  ssabral  3227  rabss  3233  ssrabeq  3243  uniiunlem  3245  dfdif3  3246  ddifstab  3268  uncom  3280  inass  3346  indi  3383  difindiss  3390  difin2  3398  reupick3  3421  n0rf  3436  eq0  3442  eqv  3443  vss  3471  disj  3472  disj3  3476  undisj1  3481  undisj2  3482  exsnrex  3635  euabsn2  3662  euabsn  3663  prssg  3750  dfuni2  3812  unissb  3840  elint2  3852  ssint  3861  dfiin2g  3920  iunn0m  3948  iunxun  3967  iunxiun  3969  iinpw  3978  disjnim  3995  dftr2  4104  dftr5  4105  dftr3  4106  dftr4  4107  vnex  4135  inuni  4156  snelpw  4214  sspwb  4217  opelopabsb  4261  eusv2  4458  orddif  4547  onintexmid  4573  zfregfr  4574  tfi  4582  opthprc  4678  elxp3  4681  xpiundir  4686  elvv  4689  brinxp2  4694  relsn  4732  reliun  4748  inxp  4762  raliunxp  4769  rexiunxp  4770  cnvuni  4814  dm0rn0  4845  elrn  4871  ssdmres  4930  dfres2  4960  dfima2  4973  args  4998  cotr  5011  intasym  5014  asymref  5015  intirr  5016  cnv0  5033  xp11m  5068  cnvresima  5119  resco  5134  rnco  5136  coiun  5139  coass  5148  dfiota2  5180  dffun2  5227  dffun6f  5230  dffun4f  5233  dffun7  5244  dffun9  5246  funfn  5247  svrelfun  5282  imadiflem  5296  dffn2  5368  dffn3  5377  fintm  5402  dffn4  5445  dff1o4  5470  brprcneu  5509  eqfnfv3  5616  fnreseql  5627  fsn  5689  abrexco  5760  imaiun  5761  mpo2eqb  5984  elovmpo  6072  abexex  6127  releldm2  6186  fnmpo  6203  dftpos4  6264  tfrlem7  6318  0er  6569  eroveu  6626  erovlem  6627  map0e  6686  elixpconst  6706  domen  6751  reuen1  6801  xpf1o  6844  ssfilem  6875  finexdc  6902  pw1dc0el  6911  ssfirab  6933  sbthlemi10  6965  djuexb  7043  dmaddpq  7378  dmmulpq  7379  distrnqg  7386  enq0enq  7430  enq0tr  7433  nqnq0pi  7437  distrnq0  7458  prltlu  7486  prarloc  7502  genpdflem  7506  ltexprlemm  7599  ltexprlemlol  7601  ltexprlemupu  7603  ltexprlemdisj  7605  recexprlemdisj  7629  ltresr  7838  elnnz  9263  dfz2  9325  2rexuz  9582  eluz2b1  9601  elxr  9776  elixx1  9897  elioo2  9921  elioopnf  9967  elicopnf  9969  elfz1  10013  fzdifsuc  10081  fznn  10089  fzp1nel  10104  fznn0  10113  dfrp2  10264  redivap  10883  imdivap  10890  rexanre  11229  climreu  11305  prodmodc  11586  3dvdsdec  11870  3dvds2dec  11871  bezoutlembi  12006  nnwosdc  12040  isprm2  12117  isprm3  12118  isprm4  12119  pythagtriplem2  12266  elgz  12369  inffinp1  12430  isnsg4  13072  isring  13183  isbasis3g  13549  restsn  13683  lmbr  13716  txbas  13761  tx2cn  13773  elcncf1di  14069  dedekindicclemicc  14113  limcrcl  14130  bj-nnor  14489  bj-vprc  14651  ss1oel2o  14746  subctctexmid  14753  trirec0xor  14796