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  616  mpbiran  948  mpbiran2  949  3anrev  1014  an6  1357  nfand  1616  19.33b2  1677  nf3  1717  nf4dc  1718  nf4r  1719  equsalh  1774  sb6x  1827  sb5f  1852  sbidm  1899  sb5  1936  sbanv  1938  sborv  1939  sbhb  1993  sb3an  2011  sbel2x  2051  sbal1yz  2054  sbexyz  2056  eu2  2124  2eu4  2173  cleqh  2331  cleqf  2399  dcne  2413  necon3bii  2440  ne3anior  2490  r2alf  2549  r2exf  2550  r19.23t  2640  r19.26-3  2663  r19.26m  2664  r19.43  2691  rabid2  2710  isset  2809  ralv  2820  rexv  2821  reuv  2822  rmov  2823  rexcom4b  2828  ceqsex4v  2847  ceqsex8v  2849  ceqsrexv  2936  ralrab2  2971  rexrab2  2973  reu2  2994  reu3  2996  reueq  3005  2reuswapdc  3010  reuind  3011  sbc3an  3093  rmo2ilem  3122  csbcow  3138  ssalel  3215  dfss3  3216  dfss3f  3219  ssabral  3298  rabss  3304  ssrabeq  3314  uniiunlem  3316  dfdif3  3317  ddifstab  3339  uncom  3351  inass  3417  indi  3454  difindiss  3461  difin2  3469  reupick3  3492  n0rf  3507  eq0  3513  eqv  3514  vss  3542  disj  3543  disj3  3547  undisj1  3552  undisj2  3553  exsnrex  3711  euabsn2  3740  euabsn  3741  snmb  3793  prssg  3830  dfuni2  3895  unissb  3923  elint2  3935  ssint  3944  dfiin2g  4003  iunn0m  4031  iunxun  4050  iunxiun  4052  iinpw  4061  disjnim  4078  dftr2  4189  dftr5  4190  dftr3  4191  dftr4  4192  vnex  4220  inuni  4245  snelpw  4304  sspwb  4308  opelopabsb  4354  eusv2  4554  orddif  4645  onintexmid  4671  zfregfr  4672  tfi  4680  opthprc  4777  elxp3  4780  xpiundir  4785  elvv  4788  brinxp2  4793  relsn  4831  reliun  4848  inxp  4864  raliunxp  4871  rexiunxp  4872  cnvuni  4916  dm0rn0  4948  elrn  4975  ssdmres  5035  dfres2  5065  dfima2  5078  args  5105  cotr  5118  intasym  5121  asymref  5122  intirr  5123  cnv0  5140  xp11m  5175  cnvresima  5226  resco  5241  rnco  5243  coiun  5246  coass  5255  dfiota2  5287  dffun2  5336  dffun6f  5339  dffun4f  5342  dffun7  5353  dffun9  5355  funfn  5356  svrelfun  5395  imadiflem  5409  dffn2  5484  dffn3  5493  fintm  5522  dffn4  5565  dff1o4  5591  brprcneu  5632  eqfnfv3  5746  fnreseql  5757  fsn  5819  abrexco  5899  imaiun  5900  mpo2eqb  6130  elovmpo  6220  abexex  6287  releldm2  6347  fnmpo  6366  dftpos4  6428  tfrlem7  6482  0er  6735  eroveu  6794  erovlem  6795  map0e  6854  elixpconst  6874  domen  6921  reuen1  6974  xpf1o  7029  ssfilem  7061  ssfilemd  7063  finexdc  7091  pw1dc0el  7102  ssfirab  7128  sbthlemi10  7164  djuexb  7242  sspw1or2  7402  iftrueb01  7440  pw1if  7442  dmaddpq  7598  dmmulpq  7599  distrnqg  7606  enq0enq  7650  enq0tr  7653  nqnq0pi  7657  distrnq0  7678  prltlu  7706  prarloc  7722  genpdflem  7726  ltexprlemm  7819  ltexprlemlol  7821  ltexprlemupu  7823  ltexprlemdisj  7825  recexprlemdisj  7849  ltresr  8058  elnnz  9488  dfz2  9551  2rexuz  9815  eluz2b1  9834  elxr  10010  elixx1  10131  elioo2  10155  elioopnf  10201  elicopnf  10203  elfz1  10247  fzdifsuc  10315  fznn  10323  fzp1nel  10338  fznn0  10347  dfrp2  10522  redivap  11434  imdivap  11441  rexanre  11780  climreu  11857  prodmodc  12138  3dvdsdec  12425  3dvds2dec  12426  bitsval  12503  bezoutlembi  12575  nnwosdc  12609  isprm2  12688  isprm3  12689  isprm4  12690  pythagtriplem2  12838  elgz  12943  inffinp1  13049  isnsg4  13798  isrng  13946  isring  14012  dfrhm2  14167  lss1d  14396  isbasis3g  14769  restsn  14903  lmbr  14936  txbas  14981  tx2cn  14993  elcncf1di  15302  dedekindicclemicc  15355  limcrcl  15381  isclwwlk  16244  clwwlkccatlem  16250  eupth2lem1  16308  bj-nnor  16330  bj-vprc  16491  ss1oel2o  16586  subctctexmid  16601  trirec0xor  16649