Theorem syl6bbr 271

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

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

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 190

This theorem is referenced by:  3bitr4g  296  bibi2i  320  mtt  346  nbn2  352  rbaibr  921  ifptru  994  3bior1fd  1403  3biant1d  1406  clelab  2596  eueq3  3201  n0moeu  3736  sbcel12  3776  sbceqg  3777  sbcne12  3779  reldisj  3812  raldifeq  3848  r19.3rz  3851  r19.3rzv  3853  r19.9rzv  3854  eldifpr  3982  eldiftp  4006  reusv2lem5  4606  otthg  4685  2rbropap  4742  rabxp  4876  elrng  5031  iss  5158  elimasni  5201  eliniseg  5203  xpcan  5279  xpcan2  5280  elpredg  5401  ordelpss  5458  fcnvres  5773  dffv3  5875  funimass4  5930  fndmdif  6001  fneqeql  6005  funimass3  6013  elrnrexdmb  6042  dff4  6051  fnsnb  6099  fconst4  6145  elunirn  6174  f12dfv  6190  riota1  6288  riota2df  6290  f1ocnvfv3  6304  eqfnov  6421  elrnmpt2res  6429  caoftrn  6585  ordsucun  6671  dflim3  6693  dfom2  6713  peano5  6735  opiota  6871  suppssr  6965  mpt2xopovel  6985  brtpos  7000  rntpos  7004  ordgt0ge1  7217  ondif2  7222  oelim2  7314  omabs  7366  iiner  7453  erinxp  7455  qliftfun  7466  ordunifi  7839  elfi2  7946  elfiun  7962  fifo  7964  noinfep  8183  cantnflem1  8212  cantnf  8216  rankonidlem  8317  r1pwALT  8335  pr2nelem  8453  cardalephex  8539  alephinit  8544  dfac5lem4  8575  cflim2  8711  cfsmolem  8718  compssiso  8822  fin1a2lem11  8858  itunisuc  8867  axdclem  8967  brdom6disj  8978  alephreg  9025  fpwwe2lem9  9081  pwfseqlem3  9103  pwfseqlem4  9105  indpi  9350  nqereu  9372  ordpinq  9386  ltanq  9414  ltmnq  9415  suplem2pr  9496  map2psrpr  9552  ssxr  9721  letri3  9737  leltne  9741  ltneg  10135  leneg  10138  suprnub  10594  negiso  10609  infmrgelbOLD  10617  elnnnn0  10937  nn0sub  10944  zrevaddcl  11006  znnsub  11007  znn0sub  11008  prime  11039  eluz2  11188  indstr  11250  eluz2b1  11253  qrevaddcl  11309  rpneg  11355  xrleltne  11467  dfle2  11469  dflt2  11470  xrletri3  11474  supxrleub  11637  infxrgelb  11646  infmxrgelbOLD  11650  ixxin  11677  iccid  11706  elicopnf  11755  iccsplit  11791  fzsplit2  11850  fzsn  11866  fzpr  11877  uzsplit  11892  preduz  11938  fvinim0ffz  12055  injresinj  12057  om2uzf1oi  12205  lt2sqi  12401  le2sqi  12402  hashsdom  12598  hashf1lem1  12659  fz1isolem  12665  ccatlcan  12882  ccatrcan  12883  2swrd2eqwrdeq  13103  trclfvcotr  13150  cnpart  13380  limsuplt  13615  limsupltOLD  13616  rlimresb  13706  mertenslem2  14018  fprod2dlem  14111  sadadd2lem2  14503  saddisjlem  14517  bitsuz  14527  gcddiv  14596  algcvgblem  14615  isprm2lem  14710  isprm3  14712  isprm5  14730  prmreclem5  14943  vdwapun  15003  vdwmc2  15008  ramcl  15066  pwsle  15468  ismre  15574  mreacs  15642  acsfn  15643  iscatd2  15665  cidpropd  15693  dfiso2  15755  oppcsect2  15762  isfunc  15847  setcinv  16063  lubeldm  16305  lubval  16308  glbeldm  16318  glbval  16321  tosso  16360  ipodrsfi  16487  acsfiindd  16501  imasmnd2  16651  submacs  16690  imasgrp2  16879  issubg  16895  resgrpisgrp  16916  subgacs  16930  eqgval  16944  gaorber  17040  symgfix2  17135  psgnran  17234  isslw  17338  sylow2alem2  17348  sylow2a  17349  sylow3lem6  17362  efgcpbllemb  17483  prmcyg  17606  gsum2d2lem  17683  gsumcom2  17685  subgdmdprd  17745  dprd2d2  17755  pgpfac1lem2  17786  pgpfac1lem4  17789  imasring  17925  drngmulne0  18075  lssle0  18251  lssacs  18268  lssats2  18301  lvecvsn0  18410  islpir  18550  isnzr2  18564  zndvds  19197  znleval  19202  znleval2  19203  lindsmm  19463  islinds3  19469  islindf4  19473  eltg2b  20051  discld  20182  opnssneib  20208  cldlp  20243  restbas  20251  leordtvallem1  20303  leordtvallem2  20304  ssidcn  20348  cnprest2  20383  lmss  20391  perfcls  20458  cmpfi  20500  1stccnp  20554  subislly  20573  hausmapdom  20592  locfindis  20622  iskgen3  20641  kgencn  20648  ptpjpre1  20663  xkoccn  20711  txrest  20723  txlm  20740  txkgen  20744  xkopt  20747  xkoinjcn  20779  imasnopn  20782  imasncld  20783  imasncls  20784  qtopcn  20806  kqfeq  20816  isr0  20829  fbfinnfr  20934  trfbas  20937  fbunfip  20962  ufileu  21012  cfinufil  21021  fmid  21053  txflf  21099  fclsrest  21117  alexsubALT  21144  tsmsres  21236  ucnima  21374  fmucndlem  21384  bldisj  21491  xmeter  21526  elbl4  21656  restmetu  21663  dscopn  21666  bl2ioo  21888  isphtpc  22103  tchcph  22289  lmmbr2  22307  lmmbrf  22310  iscau2  22325  iscauf  22328  caucfil  22331  metcld  22353  metcld2  22354  bcthlem1  22370  bcthlem4  22373  cldcss2  22474  ovolgelb  22511  ovoliunlem1  22533  ismbfcn  22666  mbfmax  22684  mbfimaopnlem  22690  i1faddlem  22730  i1fmullem  22731  i1fres  22742  i1fpos  22743  itg1climres  22751  xrge0f  22768  itgresr  22815  iblcnlem1  22824  limcun  22929  dvres  22945  mdegmullem  23106  ply1remlem  23192  plyremlem  23336  vieta1  23344  ulmcau  23429  sineq0  23555  coseq1  23556  ang180lem3  23819  cubic  23854  atandm  23881  atandm2  23882  atandm3  23883  rlimcnp  23970  rlimcnp2  23971  vmappw  24122  dchrelbas3  24245  dchrelbas4  24250  dchrsum2  24275  bposlem6  24296  dchrisumlem3  24408  pntleml  24528  istrkg3ld  24588  tgcgr4  24655  lnrot2  24748  islnopp  24860  islmib  24908  brbtwn2  25014  axsegconlem6  25031  axsegcon  25036  ax5seg  25047  axpasch  25050  axeuclid  25072  axcontlem4  25076  usgrac  25157  elusuhgra  25174  nbgrael  25233  nb3gra2nb  25262  nbcusgra  25270  wlkcomp  25332  trls  25345  istrl2  25347  is2wlk  25374  0pth  25379  0spth  25380  wlkdvspthlem  25416  0crct  25433  0cycl  25434  clwlkcomp  25570  clwlkisclwwlklem0  25595  clwlkisclwwlk  25596  el2wlkonotot0  25679  2wot2wont  25693  usg2spthonot1  25697  2spot2iun2spont  25698  isrusgra  25734  isrusgusrgcl  25740  isrusgrac  25742  0eusgraiff0rgracl  25748  rusgranumwlks  25763  eupath2lem2  25785  vdn1frgrav2  25832  vdgn1frgrav2  25833  usgreg2spot  25874  numclwwlkovgel  25895  elghomOLD  26172  nmoolb  26493  nmlno0lem  26515  ubthlem1  26593  ocsh  27017  shle0  27176  eigrei  27568  adjeu  27623  nmoplb  27641  nmfnlb  27658  eleigvec2  27692  nmlnop0iALT  27729  cnlnadjlem5  27805  adjbdln  27817  jplem2  28003  cvbr2  28017  mdsl2bi  28057  chrelat3  28105  disjunsn  28281  ofpreima  28343  funcnvmpt  28346  funcnv5mpt  28347  dfcnv2  28354  gtiso  28356  fpwrelmap  28393  infxrge0glb  28423  infxrge0glbOLD  28424  xrdifh  28437  fzsplit3  28445  toslublem  28503  tosglblem  28505  isarchi  28573  xrge0tsmsbi  28623  smatrcl  28696  unitdivcld  28781  lmxrge0  28832  isrrext  28878  issibf  29239  eulerpartlemr  29280  eulerpartlemmf  29281  eulerpartlemn  29287  dstfrvunirn  29380  ballotlemfc0  29398  ballotlemfcc  29399  bnj919  29650  bnj976  29661  bnj1542  29740  bnj150  29759  bnj151  29760  bnj607  29799  bnj852  29804  bnj873  29807  bnj938  29820  bnj1171  29881  bnj1388  29914  bnj1489  29937  subfacp1lem3  29977  subfacp1lem5  29979  erdszelem9  29994  kur14  30011  iscvm  30054  mclsax  30279  dfpo2  30466  fundmpss  30478  opelco3  30491  dfon2  30509  nofulllem1  30662  nofulllem2  30663  dfbigcup2  30737  sscoid  30751  funpartfv  30783  dfrdg4  30789  cgr3permute3  30885  segletr  30952  segleantisym  30953  seglelin  30954  fneval  31079  neibastop3  31089  eltail  31101  filnetlem4  31108  bj-hbntbi  31364  bj-sbceqgALT  31572  topdifinffinlem  31820  isbasisrelowllem1  31828  isbasisrelowllem2  31829  rdgeqoa  31843  finxpreclem4  31856  finxpsuclem  31859  phpreu  31993  cos2h  32000  tan2h  32001  poimirlem16  32020  poimirlem19  32023  poimirlem23  32027  poimirlem24  32028  poimirlem26  32030  poimirlem27  32031  mbfposadd  32052  cnambfre  32053  dvtanlemOLD  32055  itg2addnclem  32057  itg2addnc  32060  iblabsnclem  32069  ftc1anclem1  32081  ftc1anclem5  32085  caures  32153  heiborlem3  32209  heiborlem10  32216  divrngidl  32325  prtlem10  32501  prtlem16  32505  prtlem19  32514  prtex  32516  prter3  32518  islshpat  32654  lcvbr2  32659  lcvbr3  32660  lshpsmreu  32746  isat3  32944  hlrelat5N  33037  islpln5  33171  cdlemblem  33429  paddvaln0N  33437  paddval0  33446  cdlemefrs29bpre1  34035  cdlemefrs29cpre1  34036  cdlemg27b  34334  cdlemg33c  34346  cdlemg33e  34348  diaglbN  34694  cdlemm10N  34757  dicopelval2  34820  dicelval2N  34821  dihopelvalcpre  34887  dihglbcpreN  34939  dih1dimatlem  34968  dihatexv  34977  dvh4dimlem  35082  mapdpglem3  35314  hdmap14lem13  35522  hdmapglem7a  35569  isnacs2  35619  rabrenfdioph  35728  expdiophlem1  35947  pw2f1ocnv  35963  pwfi2f1o  36025  numinfctb  36033  dfacbasgrp  36038  islnr3  36045  subrgacs  36137  sdrgacs  36138  isdomn3  36152  dfhe3  36441  hashnzfzclim  36741  dvconstbi  36753  sbc3orgOLD  36963  sbcel12gOLD  36975  sbcssOLD  36977  rfcnpre3  37417  rfcnpre4  37418  unima  37502  cncfshift  37848  stoweidlem59  38032  iccpartiun  38893  oddm1evenALTV  38949  oddp1evenALTV  38950  prelpw  39140  prprrab  39218  issubgr  39507  nb3gr2nb  39622  uhgrvd00  39757  isrusgr0  39772  1wlkcpr  39831  1wlkcomp  39833  upgr2wlk  39863  upgrf1istrl  39899  clWlkcomp  39965  0Trl  40011  0pth-av  40014  0spth-av  40015  0Crct  40021  0Cycl  40022  2pthon3v-av  40065  eupth2lem2  40131  uhgrasiz  40214  isfusgracl  40246  isfusgraclALT  40248  fusgraimpclALT2  40251  usgfis  40266  usgfisALT  40270  submgmacs  40312  ismhm0  40313  iscmgmALT  40368  iscsgrpALT  40370  isrnghmmul  40401