Theorem bitr4i 186

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 131	. 2 |- ( ps <-> ch )
4	1, 3	bitri 183	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2i  207  3bitr2ri  208  3bitr4i  211  3bitr4ri  212  biancomi  268  imdistan  441  biadani  602  mpbiran  925  mpbiran2  926  3anrev  973  an6  1303  nfand  1548  19.33b2  1609  nf3  1649  nf4dc  1650  nf4r  1651  equsalh  1706  sb6x  1759  sb5f  1784  sbidm  1831  sb5  1867  sbanv  1869  sborv  1870  sbhb  1920  sb3an  1938  sbel2x  1978  sbal1yz  1981  sbexyz  1983  eu2  2050  2eu4  2099  cleqh  2257  cleqf  2324  dcne  2338  necon3bii  2365  ne3anior  2415  r2alf  2474  r2exf  2475  r19.23t  2564  r19.26-3  2587  r19.26m  2588  r19.43  2615  rabid2  2633  isset  2718  ralv  2729  rexv  2730  reuv  2731  rmov  2732  rexcom4b  2737  ceqsex4v  2755  ceqsex8v  2757  ceqsrexv  2842  ralrab2  2877  rexrab2  2879  reu2  2900  reu3  2902  reueq  2911  2reuswapdc  2916  reuind  2917  sbc3an  2998  rmo2ilem  3026  csbcow  3042  dfss2  3117  dfss3  3118  dfss3f  3120  ssabral  3199  rabss  3205  ssrabeq  3215  uniiunlem  3217  dfdif3  3218  ddifstab  3240  uncom  3252  inass  3318  indi  3355  difindiss  3362  difin2  3370  reupick3  3393  n0rf  3407  eq0  3413  eqv  3414  vss  3442  disj  3443  disj3  3447  undisj1  3452  undisj2  3453  exsnrex  3603  euabsn2  3630  euabsn  3631  prssg  3715  dfuni2  3776  unissb  3804  elint2  3816  ssint  3825  dfiin2g  3884  iunn0m  3911  iunxun  3930  iunxiun  3932  iinpw  3941  disjnim  3958  dftr2  4067  dftr5  4068  dftr3  4069  dftr4  4070  vnex  4098  inuni  4119  snelpw  4176  sspwb  4179  opelopabsb  4223  eusv2  4420  orddif  4509  onintexmid  4535  zfregfr  4536  tfi  4544  opthprc  4640  elxp3  4643  xpiundir  4648  elvv  4651  brinxp2  4656  relsn  4694  reliun  4710  inxp  4723  raliunxp  4730  rexiunxp  4731  cnvuni  4775  dm0rn0  4806  elrn  4832  ssdmres  4891  dfres2  4921  dfima2  4933  args  4958  cotr  4970  intasym  4973  asymref  4974  intirr  4975  cnv0  4992  xp11m  5027  cnvresima  5078  resco  5093  rnco  5095  coiun  5098  coass  5107  dfiota2  5139  dffun2  5183  dffun6f  5186  dffun4f  5189  dffun7  5200  dffun9  5202  funfn  5203  svrelfun  5238  imadiflem  5252  dffn2  5324  dffn3  5333  fintm  5358  dffn4  5401  dff1o4  5425  brprcneu  5464  eqfnfv3  5570  fnreseql  5580  fsn  5642  abrexco  5712  imaiun  5713  mpo2eqb  5933  elovmpo  6024  abexex  6077  releldm2  6136  fnmpo  6153  dftpos4  6213  tfrlem7  6267  0er  6517  eroveu  6574  erovlem  6575  map0e  6634  elixpconst  6654  domen  6699  reuen1  6749  xpf1o  6792  ssfilem  6823  finexdc  6850  pw1dc0el  6859  ssfirab  6881  sbthlemi10  6913  djuexb  6991  dmaddpq  7302  dmmulpq  7303  distrnqg  7310  enq0enq  7354  enq0tr  7357  nqnq0pi  7361  distrnq0  7382  prltlu  7410  prarloc  7426  genpdflem  7430  ltexprlemm  7523  ltexprlemlol  7525  ltexprlemupu  7527  ltexprlemdisj  7529  recexprlemdisj  7553  ltresr  7762  elnnz  9183  dfz2  9242  2rexuz  9499  eluz2b1  9518  elxr  9690  elixx1  9808  elioo2  9832  elioopnf  9878  elicopnf  9880  elfz1  9924  fzdifsuc  9990  fznn  9998  fzp1nel  10013  fznn0  10022  dfrp2  10173  redivap  10786  imdivap  10793  rexanre  11132  climreu  11206  prodmodc  11487  3dvdsdec  11769  3dvds2dec  11770  bezoutlembi  11905  isprm2  12010  isprm3  12011  isprm4  12012  pythagtriplem2  12157  inffinp1  12254  isbasis3g  12540  restsn  12676  lmbr  12709  txbas  12754  tx2cn  12766  elcncf1di  13062  dedekindicclemicc  13106  limcrcl  13123  bj-nnor  13407  bj-vprc  13568  ss1oel2o  13662  subctctexmid  13670  trirec0xor  13713