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  311  mtt  337  nbn2  343  rbaibr  906  3bior1fd  1336  3biant1d  1339  ifptru  1397  clelab  2546  necon2abidOLD  2658  eueq3  3224  n0moeu  3752  sbcel12  3777  sbceqg  3778  sbcne12  3780  reldisj  3813  raldifeq  3861  r19.3rz  3864  r19.3rzv  3866  r19.9rzv  3867  eldifpr  3989  eldiftp  4015  reusv2lem5  4599  otthg  4674  rabxp  4860  elrng  5015  iss  5141  elimasni  5184  eliniseg  5186  xpcan  5261  xpcan2  5262  elpredg  5381  ordelpss  5438  fcnvres  5745  dffv3  5845  funimass4  5900  fndmdif  5969  fneqeql  5973  funimass3  5981  elrnrexdmb  6014  dff4  6023  fnsnb  6070  fconst4  6117  elunirn  6144  f12dfv  6160  riota1  6258  riota2df  6260  f1ocnvfv3  6274  eqfnov  6389  elrnmpt2res  6397  caoftrn  6557  ordsucun  6643  dflim3  6665  dfom2  6685  peano5  6707  opiota  6843  suppssr  6934  mpt2xopovel  6951  brtpos  6967  rntpos  6971  ordgt0ge1  7184  ondif2  7189  oelim2  7281  omabs  7333  iiner  7420  erinxp  7422  qliftfun  7433  ordunifi  7804  elfi2  7908  elfiun  7924  fifo  7926  noinfep  8109  cantnflem1  8140  cantnf  8144  cantnfOLD  8166  rankonidlem  8278  r1pwALT  8296  pr2nelem  8414  cardalephex  8503  alephinit  8508  dfac5lem4  8539  cflim2  8675  cfsmolem  8682  compssiso  8786  fin1a2lem11  8822  itunisuc  8831  axdclem  8931  brdom6disj  8942  alephreg  8989  fpwwe2lem9  9046  pwfseqlem3  9068  pwfseqlem4  9070  indpi  9315  nqereu  9337  ordpinq  9351  ltanq  9379  ltmnq  9380  suplem2pr  9461  map2psrpr  9517  ssxr  9685  letri3  9701  leltne  9705  ltneg  10093  leneg  10096  suprnub  10546  negiso  10559  infmrgelb  10563  elnnnn0  10880  nn0sub  10887  zrevaddcl  10950  znnsub  10951  znn0sub  10952  prime  10984  eluz2  11133  indstr  11195  eluz2b1  11198  qrevaddcl  11249  rpneg  11295  xrleltne  11404  dfle2  11406  dflt2  11407  xrletri3  11411  supxrleub  11571  infmxrgelb  11579  ixxin  11599  iccid  11627  elicopnf  11674  iccsplit  11707  fzsplit2  11764  fzsn  11780  fzpr  11790  uzsplit  11805  preduz  11850  injresinj  11963  om2uzf1oi  12105  lt2sqi  12301  le2sqi  12302  hashsdom  12497  hashf1lem1  12553  fz1isolem  12559  ccatlcan  12753  ccatrcan  12754  2swrd2eqwrdeq  12947  trclfvcotr  12992  cnpart  13222  limsuplt  13451  rlimresb  13537  mertenslem2  13846  fprod2dlem  13936  sadadd2lem2  14309  saddisjlem  14323  bitsuz  14333  gcddiv  14396  algcvgblem  14415  isprm2lem  14433  isprm3  14435  isprm5  14462  prmreclem5  14647  vdwapun  14701  vdwmc2  14706  ramcl  14756  pwsle  15106  ismre  15204  mreacs  15272  acsfn  15273  iscatd2  15295  cidpropd  15323  dfiso2  15385  oppcsect2  15392  isfunc  15477  setcinv  15693  lubeldm  15935  lubval  15938  glbeldm  15948  glbval  15951  tosso  15990  ipodrsfi  16117  acsfiindd  16131  imasmnd2  16281  submacs  16320  imasgrp2  16509  issubg  16525  resgrpisgrp  16546  subgacs  16560  eqgval  16574  gaorber  16670  symgfix2  16765  psgnran  16864  isslw  16952  sylow2alem2  16962  sylow2a  16963  sylow3lem6  16976  efgcpbllemb  17097  prmcyg  17220  gsum2d2lem  17322  gsumcom2  17324  subgdmdprd  17401  dprd2d2  17413  pgpfac1lem2  17446  pgpfac1lem4  17449  imasring  17588  drngmulne0  17738  lssle0  17916  lssacs  17933  lssats2  17966  lvecvsn0  18075  islpir  18217  isnzr2  18231  zndvds  18886  znleval  18891  znleval2  18892  lindsmm  19155  islinds3  19161  islindf4  19165  eltg2b  19752  discld  19883  opnssneib  19909  cldlp  19944  restbas  19952  leordtvallem1  20004  leordtvallem2  20005  ssidcn  20049  cnprest2  20084  lmss  20092  perfcls  20159  cmpfi  20201  1stccnp  20255  subislly  20274  hausmapdom  20293  locfindis  20323  iskgen3  20342  kgencn  20349  ptpjpre1  20364  xkoccn  20412  txrest  20424  txlm  20441  txkgen  20445  xkopt  20448  xkoinjcn  20480  imasnopn  20483  imasncld  20484  imasncls  20485  qtopcn  20507  kqfeq  20517  isr0  20530  fbfinnfr  20634  trfbas  20637  fbunfip  20662  ufileu  20712  cfinufil  20721  fmid  20753  txflf  20799  fclsrest  20817  alexsubALT  20843  tsmsresOLD  20937  tsmsres  20938  ucnima  21076  fmucndlem  21086  bldisj  21193  xmeter  21228  elbl4  21371  restmetu  21382  dscopn  21386  bl2ioo  21589  isphtpc  21786  tchcph  21972  lmmbr2  21990  lmmbrf  21993  iscau2  22008  iscauf  22011  caucfil  22014  metcld  22036  metcld2  22037  bcthlem1  22055  bcthlem4  22058  cldcss2  22149  ovolgelb  22183  ovoliunlem1  22205  ismbfcn  22330  mbfmax  22348  mbfimaopnlem  22354  i1faddlem  22392  i1fmullem  22393  i1fres  22404  i1fpos  22405  itg1climres  22413  xrge0f  22430  itgresr  22477  iblcnlem1  22486  limcun  22591  dvres  22607  mdegmullem  22770  ply1remlem  22855  plyremlem  22992  vieta1  23000  ulmcau  23082  sineq0  23206  coseq1  23207  ang180lem3  23470  cubic  23505  atandm  23532  atandm2  23533  atandm3  23534  rlimcnp  23621  rlimcnp2  23622  vmappw  23771  dchrelbas3  23894  dchrelbas4  23899  dchrsum2  23924  bposlem6  23945  dchrisumlem3  24057  pntleml  24177  istrkg3ld  24237  lnrot2  24389  islnopp  24499  islmib  24543  brbtwn2  24625  axsegconlem6  24642  axsegcon  24647  ax5seg  24658  axpasch  24661  axeuclid  24683  axcontlem4  24687  usgrac  24768  elusuhgra  24785  nbgrael  24843  nb3gra2nb  24872  nbcusgra  24880  wlkcomp  24942  trls  24955  istrl2  24957  is2wlk  24984  0pth  24989  0spth  24990  wlkdvspthlem  25026  0crct  25043  0cycl  25044  clwlkcomp  25180  clwlkisclwwlklem0  25205  clwlkisclwwlk  25206  el2wlkonotot0  25289  2wot2wont  25303  usg2spthonot1  25307  2spot2iun2spont  25308  isrusgra  25344  isrusgusrgcl  25350  isrusgrac  25352  0eusgraiff0rgracl  25358  rusgranumwlks  25373  eupath2lem2  25395  vdn1frgrav2  25442  vdgn1frgrav2  25443  usgreg2spot  25484  numclwwlkovgel  25505  elghomOLD  25779  nmoolb  26100  nmlno0lem  26122  ubthlem1  26200  ocsh  26615  shle0  26774  eigrei  27166  adjeu  27221  nmoplb  27239  nmfnlb  27256  eleigvec2  27290  nmlnop0iALT  27327  cnlnadjlem5  27403  adjbdln  27415  jplem2  27601  cvbr2  27615  mdsl2bi  27655  chrelat3  27703  disjunsn  27886  ofpreima  27950  funcnvmpt  27953  funcnv5mpt  27954  dfcnv2  27961  gtiso  27963  fpwrelmap  28003  infxrge0glb  28027  xrdifh  28039  fzsplit3  28047  toslublem  28107  tosglblem  28109  isarchi  28178  xrge0tsmsbi  28229  unitdivcld  28336  lmxrge0  28387  isrrext  28433  issibf  28781  eulerpartlemr  28819  eulerpartlemmf  28820  eulerpartlemn  28826  dstfrvunirn  28919  ballotlemfc0  28937  ballotlemfcc  28938  bnj919  29152  bnj976  29163  bnj1542  29242  bnj150  29261  bnj151  29262  bnj607  29301  bnj852  29306  bnj873  29309  bnj938  29322  bnj1171  29383  bnj1388  29416  bnj1489  29439  subfacp1lem3  29479  subfacp1lem5  29481  erdszelem9  29496  kur14  29513  iscvm  29556  mclsax  29781  dfpo2  29968  fundmpss  29980  opelco3  29993  dfon2  30011  nofulllem1  30162  nofulllem2  30163  dfbigcup2  30237  sscoid  30251  funpartfv  30283  dfrdg4  30289  cgr3permute3  30385  segletr  30452  segleantisym  30453  seglelin  30454  fneval  30580  neibastop3  30590  eltail  30602  filnetlem4  30609  bj-hbntbi  30822  bj-sbceqgALT  31033  topdifinffinlem  31264  isbasisrelowllem1  31272  isbasisrelowllem2  31273  cos2h  31418  tan2h  31419  mbfposadd  31434  cnambfre  31435  dvtanlemOLD  31437  itg2addnclem  31439  itg2addnc  31442  iblabsnclem  31451  ftc1anclem1  31463  ftc1anclem5  31467  caures  31535  heiborlem3  31591  heiborlem10  31598  divrngidl  31707  prtlem10  31888  prtlem16  31892  prtlem19  31901  prtex  31903  prter3  31905  islshpat  32035  lcvbr2  32040  lcvbr3  32041  lshpsmreu  32127  isat3  32325  hlrelat5N  32418  islpln5  32552  cdlemblem  32810  paddvaln0N  32818  paddval0  32827  cdlemefrs29bpre1  33416  cdlemefrs29cpre1  33417  cdlemg27b  33715  cdlemg33c  33727  cdlemg33e  33729  diaglbN  34075  cdlemm10N  34138  dicopelval2  34201  dicelval2N  34202  dihopelvalcpre  34268  dihglbcpreN  34320  dih1dimatlem  34349  dihatexv  34358  dvh4dimlem  34463  mapdpglem3  34695  hdmap14lem13  34903  hdmapglem7a  34950  isnacs2  35000  rabrenfdioph  35109  expdiophlem1  35325  pw2f1ocnv  35341  pwfi2f1o  35406  pwfi2f1oOLD  35407  numinfctb  35416  dfacbasgrp  35421  islnr3  35428  subrgacs  35513  sdrgacs  35514  isdomn3  35528  dfhe3  35755  hashnzfzclim  36075  dvconstbi  36087  sbc3orgOLD  36323  sbcel12gOLD  36335  sbcssOLD  36337  rfcnpre3  36788  rfcnpre4  36789  unima  36816  cncfshift  37044  stoweidlem59  37209  iccpartiun  37701  oddm1evenALTV  37757  oddp1evenALTV  37758  prelpw  37932  uhgrasiz  38023  isfusgracl  38055  isfusgraclALT  38057  fusgraimpclALT2  38060  usgfis  38075  usgfisALT  38079  submgmacs  38121  ismhm0  38122  iscmgmALT  38177  iscsgrpALT  38179  isrnghmmul  38210