Theorem bitr4i 243

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

Syntax hints:   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3bitr2i  264  3bitr2ri  265  3bitr4i  268  3bitr4ri  269  imor  401  dfbi2  609  pm5.32  617  imdistan  670  imimorb  847  nbi2  862  pm5.6  878  mpbiran  884  mpbiran2  885  biluk  899  3anrev  945  nannan  1291  xorneg  1313  nic-ax  1438  nic-axALT  1439  19.43  1605  19.3v  1665  19.9vOLD  1697  equsalhwOLD  1839  nf3  1867  nf4  1868  equsal  1960  sb6x  2029  sb5f  2040  sb3an  2070  sbequ8  2079  sb5  2100  sbhb  2107  sbel2x  2125  eu2  2229  eu3  2230  eu5  2242  moanim  2260  2eu4  2287  2eu6  2289  cleqh  2450  cleqf  2514  necon3bii  2549  neor  2601  neorian  2604  r2alf  2650  r2exf  2651  r19.23t  2729  r19.26-3  2749  r19.26m  2750  r19.43  2767  rabid2  2789  isset  2864  ralv  2873  rexv  2874  reuv  2875  rmov  2876  rexcom4b  2881  ceqsex4v  2899  ceqsex8v  2901  ceqsrexv  2973  ralrab2  3003  rexrab2  3005  reu2  3025  reu3  3027  reueq  3034  2reuswap  3039  reuind  3040  2reu5lem3  3044  rmo2  3132  elun  3221  dblcompl  3228  dfss2  3263  dfss3  3264  dfss3f  3266  ssabral  3338  rabss  3344  uniiunlem  3354  sspsstri  3372  npss  3380  uncom  3409  inass  3466  nsspssun  3489  dfss4  3490  dfun2  3491  dfin2  3492  indi  3502  indifdir  3512  difin2  3517  complab  3525  reupick3  3541  necompl  3545  n0f  3559  eqv  3566  vss  3588  disj3  3596  undisj1  3603  undisj2  3604  inundif  3629  undif  3631  sscon34  3662  euabsn2  3792  euabsn  3793  pwpw0  3856  prssg  3863  ssunsn  3867  pwpr  3884  dfuni2  3894  unissb  3922  elint2  3934  ssint  3943  uniintab  3965  dfiin2g  4001  iunn0  4027  iunxun  4048  iunxiun  4049  iinpw  4055  sspwb  4119  elpw1  4145  elpw12  4146  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  eqpw1  4163  pw111  4171  eluni1g  4173  elvvk  4208  ssrelk  4212  eqrelk  4213  opkelimagekg  4272  imacok  4283  xpkvexg  4286  sikexlem  4296  dfimak2  4299  dfpw12  4302  insklem  4305  ndisjrelk  4324  dfpw2  4328  dfiota4  4373  dfaddc2  4382  dfnnc2  4396  nnc0suc  4413  elsuc  4414  addcass  4416  nnsucelrlem1  4425  nndisjeq  4430  preaddccan2lem1  4455  ltfinex  4465  ltfintrilem1  4466  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  nnpw1ex  4485  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnadjoinpw  4522  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  spfininduct  4541  vfinspsslem1  4551  vfinspss  4552  vfinncsp  4555  dfphi2  4570  dfop2lem1  4574  dfop2  4576  opeq  4620  br1stg  4731  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem6  4737  setconslem7  4738  df1st2  4739  dfswap2  4742  dfima2  4746  dfco1  4749  dfsi2  4752  brssetsn  4760  dfid3  4769  opelxp  4812  xpiundir  4819  raliunxp  4824  elxp3  4832  ssopr  4847  inxp  4864  cnvuni  4896  dmuni  4915  dm0rn0  4922  elimapw1  4945  elimapw12  4946  elimapw13  4947  elimapw11c  4949  ssdmres  4988  elres  4996  imadmrn  5009  cotr  5027  intirr  5030  cnvdif  5035  rnuni  5039  xpnz  5046  xp11  5057  dfco2  5081  resco  5086  rnco  5088  coiun  5091  coass  5098  dffun2  5120  dffun6f  5124  dffun7  5134  funfn  5137  fununi  5161  dffn2  5225  dffn3  5230  fint  5246  f1funfun  5264  dffn4  5276  dff1o2  5292  dff1o4  5295  eqfnfv3  5395  fsn  5433  abrexco  5464  imaiun  5465  dff13  5472  1stfo  5506  2ndfo  5507  cnvsi  5519  funsi  5521  oprabid  5551  eloprabga  5579  dmmpt  5684  dffn5v  5707  fnov2  5708  fnmpt2  5733  brimage  5794  fntxp  5805  otsnelsi3  5806  addcfnex  5825  funsex  5829  pw1fnf1o  5856  brfullfunop  5868  clos1induct  5881  dfnnc3  5886  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  frds  5936  ssetpov  5945  eqerlem  5961  qsexg  5983  entr  6039  fundmen  6044  unen  6049  xpen  6056  enmap1lem1  6070  enpw1pw  6076  enprmaplem1  6077  lecex  6116  elncs  6120  muccl  6133  mucex  6134  muccom  6135  mucass  6136  ncdisjeq  6149  ncssfin  6152  ovcelem1  6172  ceex  6175  ce0addcnnul  6180  cenc  6182  el2c  6192  sbthlem1  6204  sbthlem3  6206  leconnnc  6219  dflec3  6222  nclenc  6223  lenc  6224  tc11  6229  taddc  6230  letc  6232  ce2le  6234  tcfnex  6245  ncfin  6248  muc0or  6253  csucex  6260  addccan2nclem1  6264  nmembers1lem1  6269  nmembers1lem3  6271  nchoicelem3  6292  nchoicelem11  6300  nchoicelem16  6305  dmfrec  6317  fnfreclem3  6320