Theorem syl6bbr 267

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

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

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 189

This theorem is referenced by:  3bitr4g  292  bibi2i  315  mtt  341  nbn2  347  rbaibr  916  3bior1fd  1375  3biant1d  1378  ifptru  1436  clelab  2576  eueq3  3213  n0moeu  3745  sbcel12  3772  sbceqg  3773  sbcne12  3775  reldisj  3808  raldifeq  3857  r19.3rz  3860  r19.3rzv  3862  r19.9rzv  3863  eldifpr  3990  eldiftp  4015  reusv2lem5  4608  otthg  4685  rabxp  4871  elrng  5026  iss  5152  elimasni  5195  eliniseg  5197  xpcan  5273  xpcan2  5274  elpredg  5394  ordelpss  5451  fcnvres  5760  dffv3  5861  funimass4  5916  fndmdif  5986  fneqeql  5990  funimass3  5998  elrnrexdmb  6027  dff4  6036  fnsnb  6083  fconst4  6129  elunirn  6156  f12dfv  6172  riota1  6270  riota2df  6272  f1ocnvfv3  6286  eqfnov  6402  elrnmpt2res  6410  caoftrn  6566  ordsucun  6652  dflim3  6674  dfom2  6694  peano5  6716  opiota  6852  suppssr  6946  mpt2xopovel  6966  brtpos  6982  rntpos  6986  ordgt0ge1  7199  ondif2  7204  oelim2  7296  omabs  7348  iiner  7435  erinxp  7437  qliftfun  7448  ordunifi  7821  elfi2  7928  elfiun  7944  fifo  7946  noinfep  8165  cantnflem1  8194  cantnf  8198  rankonidlem  8299  r1pwALT  8317  pr2nelem  8435  cardalephex  8521  alephinit  8526  dfac5lem4  8557  cflim2  8693  cfsmolem  8700  compssiso  8804  fin1a2lem11  8840  itunisuc  8849  axdclem  8949  brdom6disj  8960  alephreg  9007  fpwwe2lem9  9063  pwfseqlem3  9085  pwfseqlem4  9087  indpi  9332  nqereu  9354  ordpinq  9368  ltanq  9396  ltmnq  9397  suplem2pr  9478  map2psrpr  9534  ssxr  9703  letri3  9719  leltne  9723  ltneg  10114  leneg  10117  suprnub  10572  negiso  10587  infmrgelbOLD  10595  elnnnn0  10913  nn0sub  10920  zrevaddcl  10982  znnsub  10983  znn0sub  10984  prime  11016  eluz2  11165  indstr  11227  eluz2b1  11230  qrevaddcl  11286  rpneg  11332  xrleltne  11444  dfle2  11446  dflt2  11447  xrletri3  11451  supxrleub  11612  infxrgelb  11621  infmxrgelbOLD  11625  ixxin  11652  iccid  11681  elicopnf  11730  iccsplit  11765  fzsplit2  11824  fzsn  11840  fzpr  11851  uzsplit  11866  preduz  11911  injresinj  12025  om2uzf1oi  12167  lt2sqi  12363  le2sqi  12364  hashsdom  12560  hashf1lem1  12618  fz1isolem  12624  ccatlcan  12828  ccatrcan  12829  2swrd2eqwrdeq  13028  trclfvcotr  13073  cnpart  13303  limsuplt  13538  limsupltOLD  13539  rlimresb  13629  mertenslem2  13941  fprod2dlem  14034  sadadd2lem2  14424  saddisjlem  14438  bitsuz  14448  gcddiv  14517  algcvgblem  14536  isprm2lem  14631  isprm3  14633  isprm5  14651  prmreclem5  14864  vdwapun  14924  vdwmc2  14929  ramcl  14987  pwsle  15390  ismre  15496  mreacs  15564  acsfn  15565  iscatd2  15587  cidpropd  15615  dfiso2  15677  oppcsect2  15684  isfunc  15769  setcinv  15985  lubeldm  16227  lubval  16230  glbeldm  16240  glbval  16243  tosso  16282  ipodrsfi  16409  acsfiindd  16423  imasmnd2  16573  submacs  16612  imasgrp2  16801  issubg  16817  resgrpisgrp  16838  subgacs  16852  eqgval  16866  gaorber  16962  symgfix2  17057  psgnran  17156  isslw  17260  sylow2alem2  17270  sylow2a  17271  sylow3lem6  17284  efgcpbllemb  17405  prmcyg  17528  gsum2d2lem  17605  gsumcom2  17607  subgdmdprd  17667  dprd2d2  17677  pgpfac1lem2  17708  pgpfac1lem4  17711  imasring  17847  drngmulne0  17997  lssle0  18173  lssacs  18190  lssats2  18223  lvecvsn0  18332  islpir  18473  isnzr2  18487  zndvds  19120  znleval  19125  znleval2  19126  lindsmm  19386  islinds3  19392  islindf4  19396  eltg2b  19974  discld  20105  opnssneib  20131  cldlp  20166  restbas  20174  leordtvallem1  20226  leordtvallem2  20227  ssidcn  20271  cnprest2  20306  lmss  20314  perfcls  20381  cmpfi  20423  1stccnp  20477  subislly  20496  hausmapdom  20515  locfindis  20545  iskgen3  20564  kgencn  20571  ptpjpre1  20586  xkoccn  20634  txrest  20646  txlm  20663  txkgen  20667  xkopt  20670  xkoinjcn  20702  imasnopn  20705  imasncld  20706  imasncls  20707  qtopcn  20729  kqfeq  20739  isr0  20752  fbfinnfr  20856  trfbas  20859  fbunfip  20884  ufileu  20934  cfinufil  20943  fmid  20975  txflf  21021  fclsrest  21039  alexsubALT  21066  tsmsres  21158  ucnima  21296  fmucndlem  21306  bldisj  21413  xmeter  21448  elbl4  21578  restmetu  21585  dscopn  21588  bl2ioo  21810  isphtpc  22025  tchcph  22211  lmmbr2  22229  lmmbrf  22232  iscau2  22247  iscauf  22250  caucfil  22253  metcld  22275  metcld2  22276  bcthlem1  22292  bcthlem4  22295  cldcss2  22396  ovolgelb  22433  ovoliunlem1  22455  ismbfcn  22587  mbfmax  22605  mbfimaopnlem  22611  i1faddlem  22651  i1fmullem  22652  i1fres  22663  i1fpos  22664  itg1climres  22672  xrge0f  22689  itgresr  22736  iblcnlem1  22745  limcun  22850  dvres  22866  mdegmullem  23027  ply1remlem  23113  plyremlem  23257  vieta1  23265  ulmcau  23350  sineq0  23476  coseq1  23477  ang180lem3  23740  cubic  23775  atandm  23802  atandm2  23803  atandm3  23804  rlimcnp  23891  rlimcnp2  23892  vmappw  24043  dchrelbas3  24166  dchrelbas4  24171  dchrsum2  24196  bposlem6  24217  dchrisumlem3  24329  pntleml  24449  istrkg3ld  24509  tgcgr4  24576  lnrot2  24669  islnopp  24781  islmib  24829  brbtwn2  24935  axsegconlem6  24952  axsegcon  24957  ax5seg  24968  axpasch  24971  axeuclid  24993  axcontlem4  24997  usgrac  25078  elusuhgra  25095  nbgrael  25154  nb3gra2nb  25183  nbcusgra  25191  wlkcomp  25253  trls  25266  istrl2  25268  is2wlk  25295  0pth  25300  0spth  25301  wlkdvspthlem  25337  0crct  25354  0cycl  25355  clwlkcomp  25491  clwlkisclwwlklem0  25516  clwlkisclwwlk  25517  el2wlkonotot0  25600  2wot2wont  25614  usg2spthonot1  25618  2spot2iun2spont  25619  isrusgra  25655  isrusgusrgcl  25661  isrusgrac  25663  0eusgraiff0rgracl  25669  rusgranumwlks  25684  eupath2lem2  25706  vdn1frgrav2  25753  vdgn1frgrav2  25754  usgreg2spot  25795  numclwwlkovgel  25816  elghomOLD  26091  nmoolb  26412  nmlno0lem  26434  ubthlem1  26512  ocsh  26936  shle0  27095  eigrei  27487  adjeu  27542  nmoplb  27560  nmfnlb  27577  eleigvec2  27611  nmlnop0iALT  27648  cnlnadjlem5  27724  adjbdln  27736  jplem2  27922  cvbr2  27936  mdsl2bi  27976  chrelat3  28024  disjunsn  28204  ofpreima  28268  funcnvmpt  28271  funcnv5mpt  28272  dfcnv2  28279  gtiso  28281  fpwrelmap  28318  infxrge0glb  28348  infxrge0glbOLD  28349  xrdifh  28362  fzsplit3  28370  toslublem  28428  tosglblem  28430  isarchi  28499  xrge0tsmsbi  28549  smatrcl  28622  unitdivcld  28707  lmxrge0  28758  isrrext  28804  issibf  29166  eulerpartlemr  29207  eulerpartlemmf  29208  eulerpartlemn  29214  dstfrvunirn  29307  ballotlemfc0  29325  ballotlemfcc  29326  bnj919  29578  bnj976  29589  bnj1542  29668  bnj150  29687  bnj151  29688  bnj607  29727  bnj852  29732  bnj873  29735  bnj938  29748  bnj1171  29809  bnj1388  29842  bnj1489  29865  subfacp1lem3  29905  subfacp1lem5  29907  erdszelem9  29922  kur14  29939  iscvm  29982  mclsax  30207  dfpo2  30395  fundmpss  30407  opelco3  30420  dfon2  30438  nofulllem1  30591  nofulllem2  30592  dfbigcup2  30666  sscoid  30680  funpartfv  30712  dfrdg4  30718  cgr3permute3  30814  segletr  30881  segleantisym  30882  seglelin  30883  fneval  31008  neibastop3  31018  eltail  31030  filnetlem4  31037  bj-hbntbi  31298  bj-sbceqgALT  31504  topdifinffinlem  31750  isbasisrelowllem1  31758  isbasisrelowllem2  31759  rdgeqoa  31773  finxpreclem4  31786  finxpsuclem  31789  phpreu  31929  cos2h  31936  tan2h  31937  poimirlem16  31956  poimirlem19  31959  poimirlem23  31963  poimirlem24  31964  poimirlem26  31966  poimirlem27  31967  mbfposadd  31988  cnambfre  31989  dvtanlemOLD  31991  itg2addnclem  31993  itg2addnc  31996  iblabsnclem  32005  ftc1anclem1  32017  ftc1anclem5  32021  caures  32089  heiborlem3  32145  heiborlem10  32152  divrngidl  32261  prtlem10  32437  prtlem16  32441  prtlem19  32450  prtex  32452  prter3  32454  islshpat  32583  lcvbr2  32588  lcvbr3  32589  lshpsmreu  32675  isat3  32873  hlrelat5N  32966  islpln5  33100  cdlemblem  33358  paddvaln0N  33366  paddval0  33375  cdlemefrs29bpre1  33964  cdlemefrs29cpre1  33965  cdlemg27b  34263  cdlemg33c  34275  cdlemg33e  34277  diaglbN  34623  cdlemm10N  34686  dicopelval2  34749  dicelval2N  34750  dihopelvalcpre  34816  dihglbcpreN  34868  dih1dimatlem  34897  dihatexv  34906  dvh4dimlem  35011  mapdpglem3  35243  hdmap14lem13  35451  hdmapglem7a  35498  isnacs2  35548  rabrenfdioph  35657  expdiophlem1  35876  pw2f1ocnv  35892  pwfi2f1o  35954  numinfctb  35962  dfacbasgrp  35967  islnr3  35974  subrgacs  36066  sdrgacs  36067  isdomn3  36081  dfhe3  36370  hashnzfzclim  36671  dvconstbi  36683  sbc3orgOLD  36893  sbcel12gOLD  36905  sbcssOLD  36907  rfcnpre3  37354  rfcnpre4  37355  unima  37429  cncfshift  37751  stoweidlem59  37920  iccpartiun  38748  oddm1evenALTV  38804  oddp1evenALTV  38805  prelpw  38993  prprrab  39068  issubgr  39343  nb3gr2nb  39458  uhgrvd00  39571  isrusgr0  39583  1wlkcpr  39642  1wlkcomp  39643  upgr2wlk  39664  upgrf1istrl  39673  0Trl  39710  uhgrasiz  39759  isfusgracl  39791  isfusgraclALT  39793  fusgraimpclALT2  39796  usgfis  39811  usgfisALT  39815  submgmacs  39857  ismhm0  39858  iscmgmALT  39913  iscsgrpALT  39915  isrnghmmul  39946