Theorem syl6bbr 263

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 202	. 2 |- ( ch <-> th )
4	1, 3	syl6bb 261	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 184

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 185

This theorem is referenced by:  3bitr4g  288  bibi2i  313  mtt  339  nbn2  345  rbaibr  903  3bior1fd  1333  3biant1d  1336  clelab  2585  necon2abidOLD  2696  eueq3  3258  n0moeu  3780  sbcel12  3805  sbcel12gOLD  3806  sbceqg  3807  sbcne12  3809  sbcne12gOLD  3810  reldisj  3852  raldifeq  3899  r19.3rz  3902  r19.3rzv  3904  r19.9rzv  3905  eldifpr  4027  eldiftp  4053  reusv2lem5  4638  otthg  4716  ordelpss  4892  rabxp  5022  elrng  5180  iss  5307  elimasni  5350  eliniseg  5352  xpcan  5429  xpcan2  5430  fcnvres  5748  dffv3  5848  funimass4  5905  fndmdif  5972  fneqeql  5976  funimass3  5984  elrnrexdmb  6017  dff4  6026  fnsnb  6071  fconst4  6117  elunirn  6144  f12dfv  6160  riota1  6257  riota2df  6259  f1ocnvfv3  6273  eqfnov  6389  elrnmpt2res  6397  caoftrn  6556  ordsucun  6641  dflim3  6663  dfom2  6683  peano5  6704  opiota  6840  suppssr  6929  mpt2xopovel  6946  brtpos  6962  rntpos  6966  ordgt0ge1  7145  ondif2  7150  oelim2  7242  omabs  7294  iiner  7381  erinxp  7383  qliftfun  7394  ordunifi  7768  elfi2  7872  elfiun  7888  fifo  7890  noinfep  8074  cantnflem1  8106  cantnf  8110  cantnfOLD  8132  rankonidlem  8244  r1pwOLD  8262  pr2nelem  8380  cardalephex  8469  alephinit  8474  dfac5lem4  8505  cflim2  8641  cfsmolem  8648  compssiso  8752  fin1a2lem11  8788  itunisuc  8797  axdclem  8897  brdom6disj  8908  alephreg  8955  fpwwe2lem9  9014  pwfseqlem3  9036  pwfseqlem4  9038  indpi  9283  nqereu  9305  ordpinq  9319  ltanq  9347  ltmnq  9348  suplem2pr  9429  map2psrpr  9485  ssxr  9652  letri3  9668  leltne  9672  ltneg  10053  leneg  10056  suprnub  10507  negiso  10520  infmrgelb  10524  elnnnn0  10840  nn0sub  10847  zrevaddcl  10910  znnsub  10911  znn0sub  10912  prime  10944  eluz2  11091  indstr  11154  eluz2b1  11157  qrevaddcl  11208  rpneg  11253  xrleltne  11355  dfle2  11357  dflt2  11358  xrletri3  11362  supxrleub  11522  infmxrgelb  11530  ixxin  11550  iccid  11578  elicopnf  11624  iccsplit  11657  fzsplit2  11714  fzsn  11729  fzpr  11739  uzsplit  11754  injresinj  11900  om2uzf1oi  12038  lt2sqi  12230  le2sqi  12231  hashsdom  12423  hashf1lem1  12478  fz1isolem  12484  ccatlcan  12671  ccatrcan  12672  2swrd2eqwrdeq  12865  cnpart  13047  limsuplt  13276  rlimresb  13362  mertenslem2  13668  sadadd2lem2  13972  saddisjlem  13986  bitsuz  13996  gcddiv  14059  algcvgblem  14078  isprm2lem  14096  isprm3  14098  isprm5  14125  prmreclem5  14310  vdwapun  14364  vdwmc2  14369  ramcl  14419  pwsle  14761  ismre  14859  mreacs  14927  acsfn  14928  iscatd2  14950  cidpropd  14977  oppcsect2  15041  isfunc  15102  setcinv  15286  lubeldm  15480  lubval  15483  glbeldm  15493  glbval  15496  tosso  15535  ipodrsfi  15662  acsfiindd  15676  imasmnd2  15826  submacs  15865  imasgrp2  16054  issubg  16070  resgrpisgrp  16091  subgacs  16105  eqgval  16119  gaorber  16215  symgfix2  16310  psgnran  16409  isslw  16497  sylow2alem2  16507  sylow2a  16508  sylow3lem6  16521  efgcpbllemb  16642  prmcyg  16765  gsum2d2lem  16870  gsumcom2  16872  subgdmdprd  16949  dprd2d2  16961  pgpfac1lem2  16994  pgpfac1lem4  16997  imasring  17136  drngmulne0  17286  lssle0  17464  lssacs  17481  lssats2  17514  lvecvsn0  17623  islpir  17765  isnzr2  17779  zndvds  18455  znleval  18460  znleval2  18461  lindsmm  18730  islinds3  18736  islindf4  18740  eltg2b  19327  discld  19456  opnssneib  19482  cldlp  19517  restbas  19525  leordtvallem1  19577  leordtvallem2  19578  ssidcn  19622  cnprest2  19657  lmss  19665  perfcls  19732  cmpfi  19774  1stccnp  19829  subislly  19848  hausmapdom  19867  locfindis  19897  iskgen3  19916  kgencn  19923  ptpjpre1  19938  xkoccn  19986  txrest  19998  txlm  20015  txkgen  20019  xkopt  20022  xkoinjcn  20054  imasnopn  20057  imasncld  20058  imasncls  20059  qtopcn  20081  kqfeq  20091  isr0  20104  fbfinnfr  20208  trfbas  20211  fbunfip  20236  ufileu  20286  cfinufil  20295  fmid  20327  txflf  20373  fclsrest  20391  alexsubALT  20417  tsmsresOLD  20511  tsmsres  20512  ucnima  20650  fmucndlem  20660  bldisj  20767  xmeter  20802  elbl4  20945  restmetu  20956  dscopn  20960  bl2ioo  21163  isphtpc  21360  tchcph  21546  lmmbr2  21564  lmmbrf  21567  iscau2  21582  iscauf  21585  caucfil  21588  metcld  21610  metcld2  21611  bcthlem1  21629  bcthlem4  21632  cldcss2  21723  ovolgelb  21757  ovoliunlem1  21779  ismbfcn  21904  mbfmax  21922  mbfimaopnlem  21928  i1faddlem  21966  i1fmullem  21967  i1fres  21978  i1fpos  21979  itg1climres  21987  xrge0f  22004  itgresr  22051  iblcnlem1  22060  limcun  22165  dvres  22181  mdegmullem  22344  ply1remlem  22429  plyremlem  22565  vieta1  22573  ulmcau  22655  sineq0  22779  coseq1  22780  ang180lem3  23008  cubic  23045  atandm  23072  atandm2  23073  atandm3  23074  rlimcnp  23160  rlimcnp2  23161  vmappw  23255  dchrelbas3  23378  dchrelbas4  23383  dchrsum2  23408  bposlem6  23429  dchrisumlem3  23541  pntleml  23661  lnrot2  23869  islnopp  23978  islmib  24018  brbtwn2  24073  axsegconlem6  24090  axsegcon  24095  ax5seg  24106  axpasch  24109  axeuclid  24131  axcontlem4  24135  usgrac  24216  elusuhgra  24233  nbgrael  24291  nb3gra2nb  24320  nbcusgra  24328  wlkcomp  24390  trls  24403  istrl2  24405  is2wlk  24432  0pth  24437  0spth  24438  wlkdvspthlem  24474  0crct  24491  0cycl  24492  clwlkcomp  24628  clwlkisclwwlklem0  24653  clwlkisclwwlk  24654  el2wlkonotot0  24737  2wot2wont  24751  usg2spthonot1  24755  2spot2iun2spont  24756  isrusgra  24792  isrusgusrgcl  24798  isrusgrac  24800  0eusgraiff0rgracl  24806  rusgranumwlks  24821  eupath2lem2  24843  vdn1frgrav2  24890  vdgn1frgrav2  24891  usgreg2spot  24932  numclwwlkovgel  24953  elghomOLD  25230  nmoolb  25551  nmlno0lem  25573  ubthlem1  25651  ocsh  26066  shle0  26225  eigrei  26618  adjeu  26673  nmoplb  26691  nmfnlb  26708  eleigvec2  26742  nmlnop0iALT  26779  cnlnadjlem5  26855  adjbdln  26867  jplem2  27053  cvbr2  27067  mdsl2bi  27107  chrelat3  27155  disjunsn  27318  ofpreima  27372  funcnvmpt  27375  funcnv5mpt  27376  dfcnv2  27382  gtiso  27384  fpwrelmap  27421  xrdifh  27456  fzsplit3  27464  toslublem  27521  tosglblem  27523  isarchi  27592  xrge0tsmsbi  27642  unitdivcld  27749  lmxrge0  27800  isrrext  27847  issibf  28141  eulerpartlemr  28179  eulerpartlemmf  28180  eulerpartlemn  28186  dstfrvunirn  28279  ballotlemfc0  28297  ballotlemfcc  28298  subfacp1lem3  28492  subfacp1lem5  28494  erdszelem9  28509  kur14  28526  iscvm  28570  mclsax  28795  fprod2dlem  29078  dfpo2  29152  fundmpss  29164  opelco3  29176  dfon2  29192  elpredg  29226  preduz  29248  nofulllem1  29430  nofulllem2  29431  dfbigcup2  29517  sscoid  29531  funpartfv  29563  dfrdg4  29568  cgr3permute3  29665  segletr  29732  segleantisym  29733  seglelin  29734  cos2h  30014  tan2h  30015  mbfposadd  30030  cnambfre  30031  dvtanlem  30032  itg2addnclem  30034  itg2addnc  30037  iblabsnclem  30046  ftc1anclem1  30058  ftc1anclem5  30062  fneval  30138  neibastop3  30148  eltail  30160  filnetlem4  30167  caures  30221  heiborlem3  30277  heiborlem10  30284  divrngidl  30393  prtlem10  30574  prtlem16  30578  prtlem19  30587  prtex  30589  prter3  30591  isnacs2  30606  rabrenfdioph  30716  expdiophlem1  30931  pw2f1ocnv  30947  pwfi2f1o  31012  numinfctb  31020  dfacbasgrp  31025  islnr3  31032  subrgacs  31118  sdrgacs  31119  isdomn3  31133  hashnzfzclim  31196  dvconstbi  31208  rfcnpre3  31355  rfcnpre4  31356  unima  31387  cncfshift  31579  stoweidlem59  31726  prelpw  32133  uhgrasiz  32228  isfusgracl  32260  isfusgraclALT  32262  fusgraimpclALT2  32265  usgfis  32280  usgfisALT  32284  submgmacs  32326  iscmgmALT  32381  iscsgrpALT  32383  isrnghmmul  32407  sbc3orgOLD  33011  sbcssOLD  33021  bnj919  33532  bnj976  33543  bnj1542  33622  bnj150  33641  bnj151  33642  bnj607  33681  bnj852  33686  bnj873  33689  bnj938  33702  bnj1171  33763  bnj1388  33796  bnj1489  33819  bj-hbntbi  33972  bj-sbceqgALT  34181  islshpat  34444  lcvbr2  34449  lcvbr3  34450  lshpsmreu  34536  isat3  34734  hlrelat5N  34827  islpln5  34961  cdlemblem  35219  paddvaln0N  35227  paddval0  35236  cdlemefrs29bpre1  35825  cdlemefrs29cpre1  35826  cdlemg27b  36124  cdlemg33c  36136  cdlemg33e  36138  diaglbN  36484  cdlemm10N  36547  dicopelval2  36610  dicelval2N  36611  dihopelvalcpre  36677  dihglbcpreN  36729  dih1dimatlem  36758  dihatexv  36767  dvh4dimlem  36872  mapdpglem3  37104  hdmap14lem13  37312  hdmapglem7a  37359