Theorem syl6bbr 263

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-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  3bior1fd  1317  3biant1d  1320  necon2abid  2658  eueq3  3123  n0moeu  3638  sbcel12  3663  sbcel12gOLD  3664  sbceqg  3665  sbcne12  3667  sbcne12gOLD  3668  reldisj  3710  raldifeq  3756  r19.3rz  3759  r19.3rzv  3761  r19.9rzv  3762  eldifpr  3882  eldiftp  3907  reusv2lem5  4485  ordelpss  4734  rabxp  4862  elrng  5018  iss  5142  elimasni  5184  eliniseg  5186  xpcan  5262  xpcan2  5263  fcnvres  5576  dffv3  5675  funimass4  5730  fndmdif  5795  fneqeql  5799  funimass3  5807  elrnrexdmb  5836  dff4  5845  fconst4  5929  elunirnALT  5957  riota1  6059  riota2df  6061  f1ocnvfv3  6075  eqfnov  6185  elrnmpt2res  6193  caoftrn  6344  ordsucun  6425  dflim3  6447  dfom2  6467  peano5  6488  opiota  6622  suppssr  6709  mpt2xopovel  6726  brtpos  6743  rntpos  6747  ordgt0ge1  6925  ondif2  6930  oelim2  7022  omabs  7074  iiner  7160  erinxp  7162  qliftfun  7173  ordunifi  7550  elfi2  7652  elfiun  7668  fifo  7670  noinfep  7853  cantnfrescl  7872  cantnflem1  7885  cantnf  7889  cantnfOLD  7911  rankonidlem  8023  r1pwOLD  8041  pr2nelem  8159  cardalephex  8248  alephinit  8253  dfac5lem4  8284  cflim2  8420  cfsmolem  8427  compssiso  8531  fin1a2lem11  8567  itunisuc  8576  axdclem  8676  brdom6disj  8687  alephreg  8734  fpwwe2lem9  8792  pwfseqlem3  8814  pwfseqlem4  8816  indpi  9063  nqereu  9085  ordpinq  9099  ltanq  9127  ltmnq  9128  suplem2pr  9209  map2psrpr  9264  ssxr  9431  letri3  9447  leltne  9451  ltneg  9826  leneg  9829  suprnub  10280  negiso  10293  infmrgelb  10297  elnnnn0  10610  nn0sub  10617  zrevaddcl  10677  znnsub  10678  znn0sub  10679  prime  10709  eluz2  10854  indstr  10910  eluz2b1  10913  qrevaddcl  10962  rpneg  11007  xrleltne  11109  dfle2  11111  dflt2  11112  xrletri3  11116  supxrleub  11276  infmxrgelb  11284  ixxin  11304  iccid  11332  elicopnf  11372  iccsplit  11404  fzsplit2  11460  fzsn  11486  fzpr  11495  uzsplit  11513  injresinj  11622  om2uzf1oi  11759  lt2sqi  11937  le2sqi  11938  hashsdom  12127  hashf1lem1  12191  fz1isolem  12197  ccatlcan  12349  ccatrcan  12350  2swrd2eqwrdeq  12536  cnpart  12712  limsuplt  12940  rlimresb  13026  mertenslem2  13327  sadadd2lem2  13628  saddisjlem  13642  bitsuz  13652  gcddiv  13715  algcvgblem  13734  isprm2lem  13752  isprm3  13754  isprm5  13780  prmreclem5  13963  vdwapun  14017  vdwmc2  14022  ramcl  14072  pwsle  14412  ismre  14510  mreacs  14578  acsfn  14579  iscatd2  14601  cidpropd  14631  oppcsect2  14695  isfunc  14756  setcinv  14940  lubeldm  15133  lubval  15136  glbeldm  15146  glbval  15149  tosso  15188  ipodrsfi  15315  acsfiindd  15329  imasmnd2  15440  submacs  15474  imasgrp2  15649  issubg  15660  resgrpisgrp  15681  subgacs  15695  eqgval  15709  gaorber  15805  symgfix2  15900  psgnran  16000  isslw  16086  sylow2alem2  16096  sylow2a  16097  sylow3lem6  16110  efgcpbllemb  16231  prmcyg  16349  gsum2d2lem  16438  gsumcom2  16440  subgdmdprd  16504  dprd2d2  16516  pgpfac1lem2  16549  pgpfac1lem4  16552  imasrng  16645  drngmulne0  16777  lssle0  16952  lssacs  16969  lssats2  17002  lvecvsn0  17111  islpir  17252  isnzr2  17266  zndvds  17823  znleval  17828  znleval2  17829  lindsmm  18098  islinds3  18104  islindf4  18108  eltg2b  18405  discld  18534  opnssneib  18560  cldlp  18595  restbas  18603  leordtvallem1  18655  leordtvallem2  18656  ssidcn  18700  cnprest2  18735  lmss  18743  perfcls  18810  cmpfi  18852  1stccnp  18907  subislly  18926  hausmapdom  18945  iskgen3  18963  kgencn  18970  ptpjpre1  18985  xkoccn  19033  txrest  19045  txlm  19062  txkgen  19066  xkopt  19069  xkoinjcn  19101  imasnopn  19104  imasncld  19105  imasncls  19106  qtopcn  19128  kqfeq  19138  isr0  19151  fbfinnfr  19255  trfbas  19258  fbunfip  19283  ufileu  19333  cfinufil  19342  fmid  19374  txflf  19420  fclsrest  19438  alexsubALT  19464  tsmsresOLD  19558  tsmsres  19559  ucnima  19697  fmucndlem  19707  bldisj  19814  xmeter  19849  elbl4  19992  metuel2  19995  restmetu  20003  dscopn  20007  bl2ioo  20210  isphtpc  20407  tchcph  20593  lmmbr2  20611  lmmbrf  20614  iscau2  20629  iscauf  20632  caucfil  20635  metcld  20657  metcld2  20658  bcthlem1  20676  bcthlem4  20679  cldcss2  20770  ovolgelb  20804  ovoliunlem1  20826  ismbfcn  20950  mbfmax  20968  mbfimaopnlem  20974  i1faddlem  21012  i1fmullem  21013  i1fres  21024  i1fpos  21025  itg1climres  21033  xrge0f  21050  itgresr  21097  iblcnlem1  21106  limcun  21211  dvres  21227  mdegmullem  21433  ply1remlem  21518  plyremlem  21654  vieta1  21662  ulmcau  21744  sineq0  21867  coseq1  21868  ang180lem3  22091  cubic  22128  atandm  22155  atandm2  22156  atandm3  22157  rlimcnp  22243  rlimcnp2  22244  vmappw  22338  dchrelbas3  22461  dchrelbas4  22466  dchrsum2  22491  bposlem6  22512  dchrisumlem3  22624  pntleml  22744  lnrot2  22904  brbtwn2  22973  axsegconlem6  22990  axsegcon  22995  ax5seg  23006  axpasch  23009  axeuclid  23031  axcontlem4  23035  nbgrael  23159  nb3gra2nb  23185  nbcusgra  23193  trls  23257  istrl2  23259  is2wlk  23286  0pth  23291  0spth  23292  wlkdvspthlem  23328  0crct  23334  0cycl  23335  eupath2lem2  23421  elghom  23672  nmoolb  23993  nmlno0lem  24015  ubthlem1  24093  ocsh  24508  shle0  24667  eigrei  25060  adjeu  25115  nmoplb  25133  nmfnlb  25150  eleigvec2  25184  nmlnop0iALT  25221  cnlnadjlem5  25297  adjbdln  25309  jplem2  25495  cvbr2  25509  mdsl2bi  25549  chrelat3  25597  disjunsn  25759  ofpreima  25807  funcnvmpt  25810  funcnv5mpt  25811  dfcnv2  25817  gtiso  25819  fpwrelmap  25857  xrdifh  25892  fzsplit3  25900  toslublem  25950  tosglblem  25952  isarchi  26022  xrge0tsmsbi  26106  unitdivcld  26184  lmxrge0  26235  isrrext  26282  issibf  26566  eulerpartlemr  26604  eulerpartlemn  26611  dstfrvunirn  26704  ballotlemfc0  26722  ballotlemfcc  26723  subfacp1lem3  26917  subfacp1lem5  26919  erdszelem9  26934  kur14  26951  iscvm  26995  dfpo2  27411  fundmpss  27423  opelco3  27435  dfon2  27451  elpredg  27485  preduz  27507  nofulllem1  27689  nofulllem2  27690  dfbigcup2  27776  sscoid  27790  funpartfv  27822  dfrdg4  27827  cgr3permute3  27924  segletr  27991  segleantisym  27992  seglelin  27993  cos2h  28264  tan2h  28265  mbfposadd  28280  cnambfre  28281  dvtanlem  28282  itg2addnclem  28284  itg2addnc  28287  iblabsnclem  28296  ftc1anclem1  28308  ftc1anclem5  28312  fneval  28400  locfindis  28418  neibastop3  28424  eltail  28436  filnetlem4  28443  caures  28497  heiborlem3  28553  heiborlem10  28560  divrngidl  28669  prtlem10  28852  prtlem16  28856  prtlem19  28865  prtex  28867  prter3  28869  isnacs2  28884  rabrenfdioph  28995  expdiophlem1  29212  pw2f1ocnv  29228  pwfi2f1o  29293  numinfctb  29301  dfacbasgrp  29306  islnr3  29313  subrgacs  29399  sdrgacs  29400  isdomn3  29414  dvconstbi  29450  rfcnpre3  29597  rfcnpre4  29598  stoweidlem59  29697  otthg  29973  f12dfv  29989  wlkcomp  30129  el2wlkonotot0  30234  2wot2wont  30248  usg2spthonot1  30252  2spot2iun2spont  30253  clwlkcomp  30269  clwlkisclwwlklem0  30293  clwlkisclwwlk  30294  isrusgra  30387  rusgranumwlks  30417  vdn1frgrav2  30461  vdgn1frgrav2  30462  usgreg2spot  30503  numclwwlkovgel  30524  sbc3orgOLD  30936  sbcssOLD  30947  bnj919  31459  bnj976  31470  bnj1542  31549  bnj150  31568  bnj151  31569  bnj607  31608  bnj852  31613  bnj873  31616  bnj938  31629  bnj1171  31690  bnj1388  31723  bnj1489  31746  bj-sbceqgALT  31995  islshpat  32232  lcvbr2  32237  lcvbr3  32238  lshpsmreu  32324  isat3  32522  hlrelat5N  32615  islpln5  32749  cdlemblem  33007  paddvaln0N  33015  paddval0  33024  cdlemefrs29bpre1  33611  cdlemefrs29cpre1  33612  cdlemg27b  33910  cdlemg33c  33922  cdlemg33e  33924  diaglbN  34270  cdlemm10N  34333  dicopelval2  34396  dicelval2N  34397  dihopelvalcpre  34463  dihglbcpreN  34515  dih1dimatlem  34544  dihatexv  34553  dvh4dimlem  34658  mapdpglem3  34890  hdmap14lem13  35098  hdmapglem7a  35145