Theorem syl6bbr 278

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
syl6bbr.1	|- ( ph -> ( ps <-> ch ) )
syl6bbr.2	|- ( th <-> ch )

Assertion

Ref	Expression
syl6bbr	|- ( ph -> ( ps <-> th ) )

Proof of Theorem syl6bbr

Step	Hyp	Ref	Expression
1		syl6bbr.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		syl6bbr.2	. . 3 |- ( th <-> ch )
3	2	bicomi 214	. 2 |- ( ch <-> th )
4	1, 3	syl6bb 276	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> 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:  3bitr4g  303  bibi2i  327  mtt  354  nbn2  360  rbaibr  946  ifptru  1023  3bior1fd  1438  3biant1d  1441  clelab  2748  eueq3  3381  n0moeu  3937  sbcel12  3983  sbceqg  3984  sbcne12  3986  reldisj  4020  raldifeq  4059  r19.3rz  4062  eldifpr  4204  eldiftp  4228  reusv2lem5  4873  prelpw  4914  otthg  4954  2rbropap  5017  rabxp  5154  elrng  5314  iss  5447  elimasni  5492  eliniseg  5494  xpcan  5570  xpcan2  5571  elpredg  5694  ordelpss  5751  fcnvres  6082  dffv3  6187  funimass4  6247  fndmdif  6321  fneqeql  6325  funimass3  6333  elrnrexdmb  6364  dff4  6373  fnsnb  6432  fconst4  6478  elunirn  6509  f12dfv  6529  riota1  6629  riota2df  6631  f1ocnvfv3  6646  eqfnov  6766  elrnmpt2res  6774  caoftrn  6932  ordsucun  7025  dflim3  7047  dfom2  7067  peano5  7089  opiota  7229  suppssr  7326  mpt2xopovel  7346  brtpos  7361  rntpos  7365  ordgt0ge1  7577  ondif2  7582  oelim2  7675  omabs  7727  iiner  7819  erinxp  7821  qliftfun  7832  mapdm0  7872  ordunifi  8210  elfi2  8320  elfiun  8336  fifo  8338  noinfep  8557  cantnflem1  8586  cantnf  8590  rankonidlem  8691  r1pwALT  8709  pr2nelem  8827  cardalephex  8913  alephinit  8918  dfac5lem4  8949  cflim2  9085  cfsmolem  9092  compssiso  9196  fin1a2lem11  9232  itunisuc  9241  axdclem  9341  brdom6disj  9354  alephreg  9404  fpwwe2lem9  9460  pwfseqlem3  9482  pwfseqlem4  9484  indpi  9729  nqereu  9751  ordpinq  9765  ltanq  9793  ltmnq  9794  suplem2pr  9875  map2psrpr  9931  ssxr  10107  letri3  10123  leltne  10127  ltneg  10528  leneg  10531  suprnub  10988  negiso  11003  elnnnn0  11336  nn0sub  11343  zrevaddcl  11422  znnsub  11423  znn0sub  11424  prime  11458  eluz2  11693  indstr  11756  eluz2b1  11759  qrevaddcl  11810  rpneg  11863  xrleltne  11978  dfle2  11980  dflt2  11981  xrletri3  11985  supxrleub  12156  infxrgelb  12165  ixxin  12192  iccid  12220  elicopnf  12269  iccsplit  12305  fzsplit2  12366  fzsn  12383  fzpr  12396  uzsplit  12412  preduz  12461  fvinim0ffz  12587  injresinj  12589  om2uzf1oi  12752  lt2sqi  12952  le2sqi  12953  hashsdom  13170  hashf1lem1  13239  fz1isolem  13245  prprrab  13255  ccatlcan  13472  ccatrcan  13473  s3eq3seq  13684  2swrd2eqwrdeq  13696  trclfvcotr  13750  cnpart  13980  limsuplt  14210  rlimresb  14296  mertenslem2  14617  fprod2dlem  14710  sadadd2lem2  15172  saddisjlem  15186  bitsuz  15196  gcddiv  15268  algcvgblem  15290  isprm3  15396  isprm5  15419  prmreclem5  15624  vdwapun  15678  vdwmc2  15683  ramcl  15733  pwsle  16152  ismre  16250  mreacs  16319  acsfn  16320  iscatd2  16342  cidpropd  16370  dfiso2  16432  oppcsect2  16439  isfunc  16524  setcinv  16740  lubeldm  16981  lubval  16984  glbeldm  16994  glbval  16997  tosso  17036  ipodrsfi  17163  acsfiindd  17177  imasmnd2  17327  submacs  17365  imasgrp2  17530  issubg  17594  resgrpisgrp  17615  subgacs  17629  eqgval  17643  gaorber  17741  symgfix2  17836  psgnran  17935  isslw  18023  sylow2alem2  18033  sylow2a  18034  sylow3lem6  18047  efgcpbllemb  18168  prmcyg  18295  gsum2d2lem  18372  gsumcom2  18374  subgdmdprd  18433  dprd2d2  18443  pgpfac1lem2  18474  pgpfac1lem4  18477  imasring  18619  drngmulne0  18769  lssle0  18950  lssacs  18967  lssats2  19000  lvecvsn0  19109  islpir  19249  isnzr2  19263  zndvds  19898  znleval  19903  znleval2  19904  lindsmm  20167  islinds3  20173  islindf4  20177  eltg2b  20763  discld  20893  opnssneib  20919  cldlp  20954  restbas  20962  leordtvallem1  21014  leordtvallem2  21015  ssidcn  21059  cnprest2  21094  lmss  21102  perfcls  21169  cmpfi  21211  1stccnp  21265  subislly  21284  hausmapdom  21303  locfindis  21333  iskgen3  21352  kgencn  21359  ptpjpre1  21374  xkoccn  21422  txrest  21434  txlm  21451  txkgen  21455  xkopt  21458  xkoinjcn  21490  imasnopn  21493  imasncld  21494  imasncls  21495  qtopcn  21517  kqfeq  21527  isr0  21540  fbfinnfr  21645  trfbas  21648  fbunfip  21673  ufileu  21723  cfinufil  21732  fmid  21764  txflf  21810  fclsrest  21828  alexsubALT  21855  tsmsres  21947  ucnima  22085  fmucndlem  22095  bldisj  22203  xmeter  22238  elbl4  22368  restmetu  22375  dscopn  22378  bl2ioo  22595  isphtpc  22793  tchcph  23036  lmmbr2  23057  lmmbrf  23060  iscau2  23075  iscauf  23078  caucfil  23081  metcld  23104  metcld2  23105  bcthlem1  23121  bcthlem4  23124  cldcss2  23213  ovolgelb  23248  ovoliunlem1  23270  ismbfcn  23398  mbfmax  23416  mbfimaopnlem  23422  i1faddlem  23460  i1fmullem  23461  i1fres  23472  i1fpos  23473  itg1climres  23481  xrge0f  23498  itgresr  23545  iblcnlem1  23554  limcun  23659  dvres  23675  mdegmullem  23838  ply1remlem  23922  plyremlem  24059  vieta1  24067  ulmcau  24149  sineq0  24273  coseq1  24274  ang180lem3  24541  cubic  24576  atandm  24603  atandm2  24604  atandm3  24605  rlimcnp  24692  rlimcnp2  24693  vmappw  24842  dchrelbas3  24963  dchrelbas4  24968  dchrsum2  24993  bposlem6  25014  dchrisumlem3  25180  pntleml  25300  istrkg3ld  25360  tgcgr4  25426  lnrot2  25519  islnopp  25631  islmib  25679  brbtwn2  25785  axsegconlem6  25802  axsegcon  25807  ax5seg  25818  axpasch  25821  axeuclid  25843  axcontlem4  25847  issubgr  26163  nb3gr2nb  26286  uhgrvd00  26430  isrusgr0  26462  wlkcpr  26524  wlkcomp  26526  upgr2wlk  26564  upgrf1istrl  26600  clwlkcomp  26675  iswwlksnx  26731  wspthsnwspthsnon  26811  wspniunwspnon  26819  2pthon3v  26839  usgr2wspthons3  26857  usgr2wspthon  26858  rusgrnumwwlks  26869  clwlkclwwlklem3  26902  clwlkclwwlk  26903  0pth  26986  eupth2lem2  27079  vdgn1frgrv2  27160  fusgreg2wsp  27200  numclwwlkovgel  27221  nmoolb  27626  nmlno0lem  27648  ubthlem1  27726  ocsh  28142  shle0  28301  eigrei  28693  adjeu  28748  nmoplb  28766  nmfnlb  28783  eleigvec2  28817  nmlnop0iALT  28854  cnlnadjlem5  28930  adjbdln  28942  jplem2  29128  cvbr2  29142  mdsl2bi  29182  chrelat3  29230  disjunsn  29407  ofpreima  29465  funcnvmpt  29468  funcnv5mpt  29469  dfcnv2  29476  gtiso  29478  fpwrelmap  29508  infxrge0glb  29530  xrdifh  29542  fzsplit3  29553  toslublem  29667  tosglblem  29669  isarchi  29736  xrge0tsmsbi  29786  smatrcl  29862  unitdivcld  29947  lmxrge0  29998  isrrext  30044  issibf  30395  eulerpartlemr  30436  eulerpartlemmf  30437  eulerpartlemn  30443  dstfrvunirn  30536  ballotlemfc0  30554  ballotlemfcc  30555  reprsuc  30693  reprpmtf1o  30704  reprdifc  30705  bnj919  30837  bnj976  30848  bnj1542  30927  bnj150  30946  bnj151  30947  bnj607  30986  bnj852  30991  bnj873  30994  bnj938  31007  bnj1171  31068  bnj1388  31101  bnj1489  31124  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem9  31181  kur14  31198  iscvm  31241  mclsax  31466  dfpo2  31645  elintfv  31662  fundmpss  31664  opelco3  31678  dfon2  31697  noetalem3  31865  dfbigcup2  32006  sscoid  32020  funpartfv  32052  dfrdg4  32058  cgr3permute3  32154  segletr  32221  segleantisym  32222  seglelin  32223  fneval  32347  neibastop3  32357  eltail  32369  filnetlem4  32376  bj-hbntbi  32695  bj-sbceqgALT  32897  bj-rest10  33041  bj-0int  33055  topdifinffinlem  33195  isbasisrelowllem1  33203  isbasisrelowllem2  33204  rdgeqoa  33218  finxpreclem4  33231  finxpsuclem  33234  uncf  33388  phpreu  33393  cos2h  33400  tan2h  33401  matunitlindflem1  33405  poimirlem16  33425  poimirlem19  33428  poimirlem23  33432  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  mbfposadd  33457  cnambfre  33458  itg2addnclem  33461  itg2addnc  33464  iblabsnclem  33473  ftc1anclem1  33485  ftc1anclem5  33489  caures  33556  heiborlem3  33612  heiborlem10  33619  elghomOLD  33686  divrngidl  33827  eqrelf  34020  brvbrvvdif  34028  eldmqsres2  34052  exanres  34063  ssrel3  34067  relcnveq  34093  iss2  34112  ecinn0  34118  prtlem10  34150  prtlem16  34154  prtlem19  34163  prtex  34165  prter3  34167  islshpat  34304  lcvbr2  34309  lcvbr3  34310  lshpsmreu  34396  isat3  34594  hlrelat5N  34687  islpln5  34821  cdlemblem  35079  paddvaln0N  35087  paddval0  35096  cdlemefrs29bpre1  35685  cdlemefrs29cpre1  35686  cdlemg27b  35984  cdlemg33c  35996  cdlemg33e  35998  diaglbN  36344  cdlemm10N  36407  dicopelval2  36470  dicelval2N  36471  dihopelvalcpre  36537  dihglbcpreN  36589  dih1dimatlem  36618  dihatexv  36627  dvh4dimlem  36732  mapdpglem3  36964  hdmap14lem13  37172  hdmapglem7a  37219  isnacs2  37269  rabrenfdioph  37378  expdiophlem1  37588  pw2f1ocnv  37604  pwfi2f1o  37666  numinfctb  37673  dfacbasgrp  37678  islnr3  37685  subrgacs  37770  sdrgacs  37771  isdomn3  37782  dfhe3  38069  clsk3nimkb  38338  ntrneiiso  38389  ntrneikb  38392  hashnzfzclim  38521  dvconstbi  38533  sbc3orgOLD  38742  sbcel12gOLD  38754  sbcssOLD  38756  rfcnpre3  39192  rfcnpre4  39193  unima  39346  cncfshift  40087  stoweidlem59  40276  nelbrnel  41293  iccpartiun  41370  oddm1evenALTV  41586  oddp1evenALTV  41587  oddprmne2  41624  submgmacs  41804  ismhm0  41805  iscmgmALT  41860  iscsgrpALT  41862  isrnghmmul  41893  elpglem2  42455