Theorem syl6bbr 266

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

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

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 188

This theorem is referenced by:  3bitr4g  291  bibi2i  314  mtt  340  nbn2  346  rbaibr  913  3bior1fd  1370  3biant1d  1373  ifptru  1431  clelab  2566  necon2abidOLD  2679  eueq3  3246  n0moeu  3775  sbcel12  3800  sbceqg  3801  sbcne12  3803  reldisj  3836  raldifeq  3885  r19.3rz  3888  r19.3rzv  3890  r19.9rzv  3891  eldifpr  4018  eldiftp  4040  reusv2lem5  4626  otthg  4701  rabxp  4887  elrng  5042  iss  5168  elimasni  5211  eliniseg  5213  xpcan  5289  xpcan2  5290  elpredg  5410  ordelpss  5467  fcnvres  5774  dffv3  5874  funimass4  5929  fndmdif  5998  fneqeql  6002  funimass3  6010  elrnrexdmb  6039  dff4  6048  fnsnb  6095  fconst4  6141  elunirn  6168  f12dfv  6184  riota1  6282  riota2df  6284  f1ocnvfv3  6298  eqfnov  6413  elrnmpt2res  6421  caoftrn  6577  ordsucun  6663  dflim3  6685  dfom2  6705  peano5  6727  opiota  6863  suppssr  6954  mpt2xopovel  6971  brtpos  6987  rntpos  6991  ordgt0ge1  7204  ondif2  7209  oelim2  7301  omabs  7353  iiner  7440  erinxp  7442  qliftfun  7453  ordunifi  7824  elfi2  7931  elfiun  7947  fifo  7949  noinfep  8167  cantnflem1  8196  cantnf  8200  rankonidlem  8301  r1pwALT  8319  pr2nelem  8437  cardalephex  8522  alephinit  8527  dfac5lem4  8558  cflim2  8694  cfsmolem  8701  compssiso  8805  fin1a2lem11  8841  itunisuc  8850  axdclem  8950  brdom6disj  8961  alephreg  9008  fpwwe2lem9  9064  pwfseqlem3  9086  pwfseqlem4  9088  indpi  9333  nqereu  9355  ordpinq  9369  ltanq  9397  ltmnq  9398  suplem2pr  9479  map2psrpr  9535  ssxr  9704  letri3  9720  leltne  9724  ltneg  10115  leneg  10118  suprnub  10573  negiso  10588  infmrgelbOLD  10596  elnnnn0  10914  nn0sub  10921  zrevaddcl  10983  znnsub  10984  znn0sub  10985  prime  11017  eluz2  11166  indstr  11228  eluz2b1  11231  qrevaddcl  11287  rpneg  11333  xrleltne  11445  dfle2  11447  dflt2  11448  xrletri3  11452  supxrleub  11613  infxrgelb  11622  infmxrgelbOLD  11626  ixxin  11653  iccid  11682  elicopnf  11731  iccsplit  11766  fzsplit2  11825  fzsn  11841  fzpr  11852  uzsplit  11867  preduz  11912  injresinj  12025  om2uzf1oi  12167  lt2sqi  12363  le2sqi  12364  hashsdom  12560  hashf1lem1  12616  fz1isolem  12622  ccatlcan  12819  ccatrcan  12820  2swrd2eqwrdeq  13017  trclfvcotr  13062  cnpart  13292  limsuplt  13526  limsupltOLD  13527  rlimresb  13617  mertenslem2  13929  fprod2dlem  14022  sadadd2lem2  14412  saddisjlem  14426  bitsuz  14436  gcddiv  14505  algcvgblem  14524  isprm2lem  14619  isprm3  14621  isprm5  14639  prmreclem5  14852  vdwapun  14912  vdwmc2  14917  ramcl  14975  pwsle  15378  ismre  15484  mreacs  15552  acsfn  15553  iscatd2  15575  cidpropd  15603  dfiso2  15665  oppcsect2  15672  isfunc  15757  setcinv  15973  lubeldm  16215  lubval  16218  glbeldm  16228  glbval  16231  tosso  16270  ipodrsfi  16397  acsfiindd  16411  imasmnd2  16561  submacs  16600  imasgrp2  16789  issubg  16805  resgrpisgrp  16826  subgacs  16840  eqgval  16854  gaorber  16950  symgfix2  17045  psgnran  17144  isslw  17248  sylow2alem2  17258  sylow2a  17259  sylow3lem6  17272  efgcpbllemb  17393  prmcyg  17516  gsum2d2lem  17593  gsumcom2  17595  subgdmdprd  17655  dprd2d2  17665  pgpfac1lem2  17696  pgpfac1lem4  17699  imasring  17835  drngmulne0  17985  lssle0  18161  lssacs  18178  lssats2  18211  lvecvsn0  18320  islpir  18461  isnzr2  18475  zndvds  19107  znleval  19112  znleval2  19113  lindsmm  19373  islinds3  19379  islindf4  19383  eltg2b  19961  discld  20092  opnssneib  20118  cldlp  20153  restbas  20161  leordtvallem1  20213  leordtvallem2  20214  ssidcn  20258  cnprest2  20293  lmss  20301  perfcls  20368  cmpfi  20410  1stccnp  20464  subislly  20483  hausmapdom  20502  locfindis  20532  iskgen3  20551  kgencn  20558  ptpjpre1  20573  xkoccn  20621  txrest  20633  txlm  20650  txkgen  20654  xkopt  20657  xkoinjcn  20689  imasnopn  20692  imasncld  20693  imasncls  20694  qtopcn  20716  kqfeq  20726  isr0  20739  fbfinnfr  20843  trfbas  20846  fbunfip  20871  ufileu  20921  cfinufil  20930  fmid  20962  txflf  21008  fclsrest  21026  alexsubALT  21053  tsmsres  21145  ucnima  21283  fmucndlem  21293  bldisj  21400  xmeter  21435  elbl4  21565  restmetu  21572  dscopn  21575  bl2ioo  21797  isphtpc  22012  tchcph  22198  lmmbr2  22216  lmmbrf  22219  iscau2  22234  iscauf  22237  caucfil  22240  metcld  22262  metcld2  22263  bcthlem1  22279  bcthlem4  22282  cldcss2  22383  ovolgelb  22420  ovoliunlem1  22442  ismbfcn  22574  mbfmax  22592  mbfimaopnlem  22598  i1faddlem  22638  i1fmullem  22639  i1fres  22650  i1fpos  22651  itg1climres  22659  xrge0f  22676  itgresr  22723  iblcnlem1  22732  limcun  22837  dvres  22853  mdegmullem  23014  ply1remlem  23100  plyremlem  23244  vieta1  23252  ulmcau  23337  sineq0  23463  coseq1  23464  ang180lem3  23727  cubic  23762  atandm  23789  atandm2  23790  atandm3  23791  rlimcnp  23878  rlimcnp2  23879  vmappw  24030  dchrelbas3  24153  dchrelbas4  24158  dchrsum2  24183  bposlem6  24204  dchrisumlem3  24316  pntleml  24436  istrkg3ld  24496  tgcgr4  24563  lnrot2  24656  islnopp  24768  islmib  24816  brbtwn2  24922  axsegconlem6  24939  axsegcon  24944  ax5seg  24955  axpasch  24958  axeuclid  24980  axcontlem4  24984  usgrac  25065  elusuhgra  25082  nbgrael  25140  nb3gra2nb  25169  nbcusgra  25177  wlkcomp  25239  trls  25252  istrl2  25254  is2wlk  25281  0pth  25286  0spth  25287  wlkdvspthlem  25323  0crct  25340  0cycl  25341  clwlkcomp  25477  clwlkisclwwlklem0  25502  clwlkisclwwlk  25503  el2wlkonotot0  25586  2wot2wont  25600  usg2spthonot1  25604  2spot2iun2spont  25605  isrusgra  25641  isrusgusrgcl  25647  isrusgrac  25649  0eusgraiff0rgracl  25655  rusgranumwlks  25670  eupath2lem2  25692  vdn1frgrav2  25739  vdgn1frgrav2  25740  usgreg2spot  25781  numclwwlkovgel  25802  elghomOLD  26077  nmoolb  26398  nmlno0lem  26420  ubthlem1  26498  ocsh  26922  shle0  27081  eigrei  27473  adjeu  27528  nmoplb  27546  nmfnlb  27563  eleigvec2  27597  nmlnop0iALT  27634  cnlnadjlem5  27710  adjbdln  27722  jplem2  27908  cvbr2  27922  mdsl2bi  27962  chrelat3  28010  disjunsn  28194  ofpreima  28258  funcnvmpt  28261  funcnv5mpt  28262  dfcnv2  28269  gtiso  28271  fpwrelmap  28312  infxrge0glb  28342  infxrge0glbOLD  28343  xrdifh  28356  fzsplit3  28364  toslublem  28423  tosglblem  28425  isarchi  28494  xrge0tsmsbi  28545  smatrcl  28618  unitdivcld  28703  lmxrge0  28754  isrrext  28800  issibf  29162  eulerpartlemr  29203  eulerpartlemmf  29204  eulerpartlemn  29210  dstfrvunirn  29303  ballotlemfc0  29321  ballotlemfcc  29322  bnj919  29574  bnj976  29585  bnj1542  29664  bnj150  29683  bnj151  29684  bnj607  29723  bnj852  29728  bnj873  29731  bnj938  29744  bnj1171  29805  bnj1388  29838  bnj1489  29861  subfacp1lem3  29901  subfacp1lem5  29903  erdszelem9  29918  kur14  29935  iscvm  29978  mclsax  30203  dfpo2  30390  fundmpss  30402  opelco3  30415  dfon2  30433  nofulllem1  30584  nofulllem2  30585  dfbigcup2  30659  sscoid  30673  funpartfv  30705  dfrdg4  30711  cgr3permute3  30807  segletr  30874  segleantisym  30875  seglelin  30876  fneval  31001  neibastop3  31011  eltail  31023  filnetlem4  31030  bj-hbntbi  31246  bj-sbceqgALT  31461  topdifinffinlem  31691  isbasisrelowllem1  31699  isbasisrelowllem2  31700  phpreu  31843  cos2h  31850  tan2h  31851  poimirlem16  31870  poimirlem19  31873  poimirlem23  31877  poimirlem24  31878  poimirlem26  31880  poimirlem27  31881  mbfposadd  31902  cnambfre  31903  dvtanlemOLD  31905  itg2addnclem  31907  itg2addnc  31910  iblabsnclem  31919  ftc1anclem1  31931  ftc1anclem5  31935  caures  32003  heiborlem3  32059  heiborlem10  32066  divrngidl  32175  prtlem10  32355  prtlem16  32359  prtlem19  32368  prtex  32370  prter3  32372  islshpat  32502  lcvbr2  32507  lcvbr3  32508  lshpsmreu  32594  isat3  32792  hlrelat5N  32885  islpln5  33019  cdlemblem  33277  paddvaln0N  33285  paddval0  33294  cdlemefrs29bpre1  33883  cdlemefrs29cpre1  33884  cdlemg27b  34182  cdlemg33c  34194  cdlemg33e  34196  diaglbN  34542  cdlemm10N  34605  dicopelval2  34668  dicelval2N  34669  dihopelvalcpre  34735  dihglbcpreN  34787  dih1dimatlem  34816  dihatexv  34825  dvh4dimlem  34930  mapdpglem3  35162  hdmap14lem13  35370  hdmapglem7a  35417  isnacs2  35467  rabrenfdioph  35576  expdiophlem1  35796  pw2f1ocnv  35812  pwfi2f1o  35874  numinfctb  35882  dfacbasgrp  35887  islnr3  35894  subrgacs  35986  sdrgacs  35987  isdomn3  36001  dfhe3  36228  hashnzfzclim  36529  dvconstbi  36541  sbc3orgOLD  36751  sbcel12gOLD  36763  sbcssOLD  36765  rfcnpre3  37215  rfcnpre4  37216  unima  37278  cncfshift  37571  stoweidlem59  37740  iccpartiun  38460  oddm1evenALTV  38516  oddp1evenALTV  38517  prelpw  38698  uhgrasiz  38978  isfusgracl  39010  isfusgraclALT  39012  fusgraimpclALT2  39015  usgfis  39030  usgfisALT  39034  submgmacs  39076  ismhm0  39077  iscmgmALT  39132  iscsgrpALT  39134  isrnghmmul  39165