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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3568  disj  3573  disj3  3577  undisj1  3582  undisj2  3583  exsnrex  3751  euabsn2  3780  euabsn  3781  snmb  3834  prssg  3872  dfuni2  3937  unissb  3965  elint2  3977  ssint  3986  dfiin2g  4045  iunn0m  4073  iunxun  4092  iunxiun  4094  iinpw  4103  disjnim  4120  dftr2  4231  dftr5  4232  dftr3  4233  dftr4  4234  vnex  4264  inuni  4291  snelpw  4352  sspwb  4356  opelopabsb  4402  eusv2  4603  orddif  4694  onintexmid  4720  zfregfr  4721  tfi  4729  opthprc  4826  elxp3  4829  xpiundir  4834  elvv  4837  brinxp2  4842  relsn  4880  reliun  4898  inxp  4914  raliunxp  4921  rexiunxp  4922  cnvuni  4966  dm0rn0  4998  elrn  5025  ssdmres  5085  dfres2  5115  dfima2  5128  args  5156  cotr  5169  intasym  5172  asymref  5173  intirr  5174  cnv0  5191  xp11m  5226  cnvresima  5277  resco  5292  rnco  5294  coiun  5297  coass  5306  dfiota2  5338  dffun2  5387  dffun6f  5390  dffun4f  5393  dffun7  5404  dffun9  5406  funfn  5407  svrelfun  5446  imadiflem  5460  dffn2  5535  dffn3  5544  fintm  5577  dffn4  5621  dff1o4  5647  brprcneu  5688  eqfnfv3  5808  fnreseql  5819  fsn  5880  abrexco  5965  imaiun  5966  mpo2eqb  6198  elovmpo  6288  abexex  6355  releldm2  6419  fnmpo  6438  cnvimadfsn  6485  dftpos4  6534  tfrlem7  6588  0er  6841  eroveu  6900  erovlem  6901  map0e  6967  elixpconst  6988  domen  7035  reuen1  7088  xpf1o  7144  ssfilem  7177  ssfilemd  7179  finexdc  7207  pw1dc0el  7218  ssfirab  7244  sbthlemi10  7283  djuexb  7384  sspw1or2  7544  iftrueb01  7582  pw1if  7584  dmaddpq  7746  dmmulpq  7747  distrnqg  7754  enq0enq  7798  enq0tr  7801  nqnq0pi  7805  distrnq0  7826  prltlu  7854  prarloc  7870  genpdflem  7874  ltexprlemm  7967  ltexprlemlol  7969  ltexprlemupu  7971  ltexprlemdisj  7973  recexprlemdisj  7997  ltresr  8206  elnnz  9654  dfz2  9717  2rexuz  9982  eluz2b1  10001  elxr  10178  elixx1  10299  elioo2  10323  elioopnf  10369  elicopnf  10371  elfz1  10416  fzdifsuc  10488  fznn  10496  fzp1nel  10511  fznn0  10520  dfrp2  10698  hashf1  11287  redivap  11639  imdivap  11646  rexanre  11986  climreu  12063  prodmodc  12345  3dvdsdec  12632  3dvds2dec  12633  bitsval  12710  bezoutlembi  12782  nnwosdc  12816  isprm2  12895  isprm3  12896  isprm4  12897  pythagtriplem2  13045  elgz  13150  inffinp1  13320  isnsg4  14015  isrng  14233  isring  14304  dfrhm2  14461  lss1d  14720  isbasis3g  15147  restsn  15281  lmbr  15314  txbas  15359  tx2cn  15371  elcncf1di  15680  dedekindicclemicc  15733  limcrcl  15759  isclwwlk  16635  clwwlkccatlem  16641  eupth2lem1  16699  bj-nnor  16762  bj-vprc  16922  ss1oel2o  17017  subctctexmid  17030  trirec0xor  17094  dfrals2  17130  dfralseu2  17164