Theorem bitr4i 267

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-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 214	. 2 |- ( ps <-> ch )
4	1, 3	bitri 264	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  3bitr2i  288  3bitr2ri  289  3bitr4i  292  3bitr4ri  293  imor  428  dfbi2  660  pm5.32  668  imdistan  725  bianass  842  imimorb  921  nbi2  936  pm5.6  951  mpbiran  953  mpbiran2  954  biluk  974  casesifp  1026  3anrev  1049  an3andi  1445  nancom  1450  nanbi  1454  xorneg  1476  cadan  1548  cadcomb  1552  nic-ax  1598  nic-axALT  1599  nf3  1712  19.43  1810  19.3v  1897  nf5  2116  nf6  2117  sb6x  2384  sb5f  2386  sb3an  2400  sbequ8ALT  2407  sb5  2430  sbhb  2438  sbnf2  2439  sbcom2  2445  eu1  2510  cleqh  2724  clelab  2748  necon3bii  2846  neor  2885  neorian  2888  r2allem  2937  r19.23t  3021  r19.26-3  3066  r19.26m  3067  r19.43  3093  rabid2  3118  rabid2f  3119  eqvf  3204  isset  3207  ralv  3219  rexv  3220  reuv  3221  rmov  3222  rexcom4b  3227  ceqsex4v  3247  ceqsex8v  3249  ceqsrexv  3336  rabtru  3361  ralrab2  3372  rexrab2  3374  reu2  3394  reu3  3396  reueq  3404  2reuswap  3410  reuind  3411  2reu5lem3  3415  sbc3an  3494  rmo2  3526  dfss2  3591  dfss3  3592  dfss3f  3595  ssabral  3673  rabss  3679  ssrabeq  3689  uniiunlem  3691  sspsstri  3709  npss  3717  raldifb  3750  uncom  3757  inass  3823  symdifass  3853  nsspssun  3857  dfss4  3858  dfun2  3859  dfin2  3860  indi  3873  indifdir  3883  difin2  3890  reupick3  3912  eq0f  3925  neq0f  3926  n0fOLD  3928  rabn0  3958  csbab  4008  vss  4012  disj  4017  disj3  4021  undisj1  4029  undisj2  4030  inundif  4046  undif  4049  rabeqsn  4214  rabsssn  4215  exsnrex  4221  euabsn2  4260  euabsn  4261  raldifsni  4324  tppreqb  4336  pwpw0  4344  prssg  4350  ssunsn  4360  pwpr  4430  dfuni2  4438  unissb  4469  elint2  4482  ssint  4493  uniintab  4515  iuneq12df  4544  dfiin2g  4553  iunn0  4580  iunxun  4605  iunxiun  4608  iinpw  4617  disjor  4634  disjxiun  4649  disjxiunOLD  4650  dftr2  4754  dftr5  4755  dftr3  4756  dftr4  4757  vprc  4796  inuni  4826  eusv2  4865  reusv2lem4  4872  rexxfr  4888  snelpw  4913  sspwb  4917  opthneg  4950  pwssun  5020  dfid3  5025  dffr2  5079  opthprc  5167  elxp3  5169  xpiundir  5174  elvv  5177  brinxp2  5180  relsn  5223  reliun  5239  inxp  5254  raliunxp  5261  cnvuni  5309  dm0rn0  5342  elrn  5366  dfres3  5403  ssdmres  5420  dfres2  5453  dfima2  5468  args  5493  dffr3  5498  cotrg  5507  intasym  5511  asymref  5512  intirr  5514  cnv0OLD  5536  xpnz  5553  xp11  5569  xpimasn  5579  resco  5639  rnco  5641  coiun  5645  coass  5654  cnvso  5674  elsnxp  5677  elsnxpOLD  5678  dffr4  5696  wfi  5713  dflim2  5781  orddif  5820  dfiota2  5852  dffun2  5898  dffun6f  5902  dffun7  5915  dffun9  5917  funfn  5918  svrelfun  5961  mptfnf  6015  dffn2  6047  dffn3  6054  fint  6084  dffn4  6121  dff1o4  6145  brprcneu  6184  eqfnfv3  6313  fnreseql  6327  fsn  6402  ftpg  6423  abrexco  6502  imaiun  6503  dff13  6512  isof1oidb  6574  isof1oopb  6575  isocnv2  6581  mpt22eqb  6769  elovmpt2  6879  sorpss  6942  abexex  7151  elxp6  7200  elxp7  7201  releldm2  7218  opiota  7229  fnmpt2  7238  frxp  7287  cnvimadfsn  7304  mpt2xneldm  7338  dftpos4  7371  wfrlem8  7422  wfrfun  7425  dfrecs3  7469  tfrlem7  7479  ondif1  7581  oarec  7642  oeeu  7683  0er  7780  0erOLD  7781  eroveu  7842  erovlem  7843  map0e  7895  elixpconst  7916  domen  7968  brsdom  7978  brdom2  7985  reuen1  8025  sbthlem10  8079  brsdom2  8084  xpf1o  8122  onfin2  8152  0sdom1dom  8158  modom  8161  unfi  8227  marypha2lem3  8343  wemapsolem  8455  sucprcreg  8506  elom3  8545  dfom5  8547  trcl  8604  epfrs  8607  rankf  8657  scottexs  8750  scott0s  8751  cplem1  8752  karden  8758  hta  8760  pm54.43lem  8825  alephsuc2  8903  iscard3  8916  aceq0  8941  aceq3lem  8943  dfac3  8944  dfac5lem2  8947  dfac5  8951  dfac7  8954  dfac12a  8970  kmlem12  8983  kmlem14  8985  kmlem15  8986  infmap2  9040  ackbij2  9065  dfacfin7  9221  ituniiun  9244  zorng  9326  brdom7disj  9353  entri2  9380  alephreg  9404  fpwwe2lem12  9463  fpwwe2lem13  9464  pwfseqlem1  9480  grutsk  9644  axgroth4  9654  grothprim  9656  grothtsk  9657  elni2  9699  ltsopi  9710  genpass  9831  psslinpr  9853  ltexprlem4  9861  ltresr  9961  1re  10039  infm3  10982  elnnz  11387  dfz2  11395  2rexuz  11740  nnwos  11755  eluz2b1  11759  qexALT  11803  elxr  11950  dflt2  11981  xrsupss  12139  xrinfmss  12140  elixx1  12184  elioo2  12216  elioopnf  12267  elicopnf  12269  elfz1  12331  fznn  12408  fzp1nel  12424  fznn0  12432  preduz  12461  prinfzo0  12506  injresinj  12589  nn0opthlem1  13055  faclbnd4lem1  13080  hashfxnn0  13124  hashfOLD  13126  hashprdifel  13186  hashfun  13224  hashf1  13241  fz1isolem  13245  f1oun2prg  13662  brtrclfv  13743  shftdm  13811  rediv  13871  imdiv  13878  rexanre  14086  caubnd  14098  climreu  14287  prodmo  14666  dvdslelem  15031  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  bitsval  15146  smueqlem  15212  algcvgblem  15290  lcmfunsnlem2  15353  isprm2  15395  isprm3  15396  isprm4  15397  pythagtriplem2  15522  elgz  15635  hashbc0  15709  0ram  15724  isstruct  15870  issect  16413  isfull2  16571  isfth2  16575  fucinv  16633  eldmcoa  16715  isdrs  16934  fpwipodrs  17164  submacs  17365  isnsg4  17637  isgim  17704  gaorb  17740  oppgid  17786  oppgsubm  17792  oppgcntz  17794  ispgp  18007  efgsdm  18143  efgcpbllema  18167  iscyg2  18284  isring  18551  isirred2  18701  opprirred  18702  dfrhm2  18717  drngid2  18763  opprsubrg  18801  islmod  18867  lss1d  18963  islmhm  19027  islmim  19062  lbsextlem2  19159  lidlnz  19228  lidldvgen  19255  isnzr2  19263  isassa  19315  dfprm2  19842  isphl  19973  elocv  20012  iunocv  20025  isobs  20064  islinds  20148  1mavmul  20354  isbasis3g  20753  fctop  20808  cctop  20810  isclo2  20892  restsn  20974  lmbr  21062  ist0-3  21149  2ndcdisj  21259  1stccnp  21265  islocfin  21320  1stckgenlem  21356  txbas  21370  ptbasin  21380  tx2cn  21413  fbfinnfr  21645  fbasrn  21688  filuni  21689  ufinffr  21733  fin1aufil  21736  rnelfmlem  21756  flimrest  21787  alexsubALTlem3  21853  alexsubALTlem4  21854  tgphaus  21920  istlm  21988  iscusp2  22106  metuel2  22370  isngp2  22401  isnlm  22479  elcncf1di  22698  isphtpc  22793  phtpcer  22794  phtpcerOLD  22795  om1elbas  22832  isclm  22864  iscvsp  22928  iscph  22970  iscau3  23076  minveclem3b  23199  elovolm  23243  ioombl1lem4  23329  dyaddisj  23364  vitali  23382  itg1climres  23481  itg2seq  23509  itg2monolem1  23517  itg2mono  23520  limcrcl  23638  lhop1  23777  itgsubst  23812  mdegleb  23824  isuc1p  23900  ismon1p  23902  plydivex  24052  ellogdm  24385  1cubr  24569  atandm2  24604  birthdaylem3  24680  dmarea  24684  dchrelbas2  24962  dchrelbas4  24968  axcontlem7  25850  nb3grpr  26284  nb3grpr2  26285  upgrwlkcompim  26539  wlkson  26552  wlkonprop  26554  wksonproplem  26601  ispth  26619  wwlknon  26742  wwlksnextinj  26794  elwspths2spth  26862  rusgrnumwwlkl1  26863  erclwwlksref  26934  frgr3v  27139  nmoubi  27627  nmobndseqi  27634  nmobndseqiALT  27635  minvecolem1  27730  isch2  28080  hlimreui  28096  isch3  28098  ocsh  28142  dfch2  28266  spanuni  28403  nonbooli  28510  5oalem7  28519  adjsym  28692  elbdop2  28730  dmadjss  28746  nmopub  28767  nmfnleub  28784  nmop0h  28850  pjssposi  29031  pjordi  29032  cvbr2  29142  cvnbtwn2  29146  mdsl2i  29181  cvmdi  29183  elat2  29199  atom1d  29212  chirredi  29253  cdj3i  29300  or3di  29307  moel  29323  mo5f  29324  2reuswap2  29328  rexunirn  29331  difrab2  29339  difininv  29354  iuneq12daf  29373  iuninc  29379  disjorf  29392  disjunsn  29407  rabfmpunirn  29453  aciunf1  29463  funcnv5mpt  29469  dfrp2  29532  eliccelico  29539  elicoelioo  29540  isomnd  29701  omndmul2  29712  isslmd  29755  hasheuni  30147  pwsiga  30193  sigainb  30199  issros  30238  2ndmbfm  30323  omssubaddlem  30361  omssubadd  30362  sitgaddlemb  30410  eulerpartlemgvv  30438  eulerpartlemn  30443  probun  30481  ballotlem2  30550  ballotlemodife  30559  bnj252  30769  bnj253  30770  bnj255  30771  bnj345  30780  bnj133  30793  bnj976  30848  bnj1098  30854  bnj121  30940  bnj130  30944  bnj150  30946  bnj581  30978  bnj607  30986  bnj865  30993  bnj917  31004  bnj934  31005  bnj964  31013  bnj983  31021  bnj996  31025  bnj1021  31034  bnj1033  31037  bnj1047  31041  bnj1049  31042  bnj1090  31047  bnj1128  31058  bnj1175  31072  bnj1189  31077  bnj1253  31085  bnj1312  31126  erdszelem9  31181  erdszelem10  31182  pconnconn  31213  cvmliftiota  31283  elmthm  31473  nepss  31599  dfso2  31644  dfpo2  31645  elrn3  31652  imaindm  31682  elpotr  31686  dfon2lem5  31692  dfon2lem7  31694  dfon2lem8  31695  frind  31740  soseq  31751  elwlim  31769  elwlimOLD  31770  wzel  31771  wzelOLD  31772  frrlem5c  31786  elno3  31808  nosgnn0  31811  nosepon  31818  nocvxminlem  31893  scutcut  31912  scutbday  31913  dmscut  31918  scutf  31919  sltrec  31924  brtxp2  31988  brpprod3a  31993  eltrans  31998  dfon3  31999  dffix2  32012  dffun10  32021  elfuns  32022  brsingle  32024  brimg  32044  funpartfun  32050  funpartfv  32052  cgrxfr  32162  segletr  32221  outsideoftr  32236  neifg  32366  filnetlem4  32376  df3nandALT1  32396  bj-consensusALT  32563  bj-biexal3  32698  bj-sb5  32768  bj-ralvw  32865  bj-rexvwv  32866  bj-rexcom4bv  32871  bj-rexcom4b  32872  bj-sbeq  32896  bj-inrab  32923  bj-xpima1snALT  32944  bj-dfmpt2a  33071  topdifinffinlem  33195  topdifinfeq  33198  relowlssretop  33211  relowlpssretop  33212  rdgeqoa  33218  wl-dfnan2  33296  wl-nannan  33298  rabiun  33382  phpreu  33393  fin2solem  33395  matunitlindflem2  33406  ptrest  33408  poimirlem25  33434  poimirlem27  33436  poimirlem30  33439  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnclem2  33462  fdc  33541  prdstotbnd  33593  isdrngo1  33755  ispridl  33833  ismaxidl  33839  impor  33880  selconj  33902  tradd  33907  scott0f  33977  biancom  33994  inxpss3  34084  idinxpssinxp2  34089  idinxpssinxp3  34090  dfrel5  34114  ineleq  34119  motr  34127  prter1  34164  islshp  34266  islshpat  34304  lcvbr2  34309  lcvnbtwn2  34314  cvrnbtwn3  34563  isatl  34586  ishlat1  34639  ishlat2  34640  cvrat4  34729  pmapglbx  35055  lhpexle3  35298  dib1dim  36454  diblsmopel  36460  lcfls1lem  36823  rexrabdioph  37358  dford4  37596  issdrg  37767  isdomn3  37782  ifpdfor2  37805  ifpdfan2  37807  ifpdfor  37809  ifpdfan  37810  ifpdfbi  37818  ifpnot23b  37827  ifpnot23c  37829  ifpnot23d  37830  ifpim123g  37845  ifpbibib  37855  clss2lem  37918  imaiun1  37943  coiun1  37944  brfvrcld2  37984  iunrelexp0  37994  brtrclfv2  38019  snhesn  38080  dffrege76  38233  frege97  38254  frege98  38255  frege109  38266  frege110  38267  dffrege115  38272  frege131  38288  frege133  38290  ntrneineine1lem  38382  ntrneiel2  38384  ntrneiiso  38389  gneispace3  38431  pm11.52  38586  pm11.58  38590  pm13.192  38611  conss34OLD  38646  impexpdcom  38721  sbc3or  38738  opelopab4  38767  uunT12p1  39027  uunT12p2  39028  uunT12p3  39029  uun2221  39040  uun2221p1  39041  uun2221p2  39042  undif3VD  39118  onfrALTlem5VD  39121  ndisj2  39218  nssrex  39260  rabssf  39302  bothtbothsame  41066  bothfbothsame  41067  aiffbtbat  41075  rmoanim  41179  2rmoswap  41184  dfodd2  41549  dfeven5  41578  dfodd7  41579  1nevenALTV  41602  oddprmne2  41624  isrng  41876  isrnghm  41892  islindeps2  42272  isldepslvec2  42274  setrec1lem3  42436  aacllem  42547