Theorem syl6bbr 255

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

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

This theorem is referenced by:  3bitr4g  280  bibi2i  305  mtt  330  nbn2  335  3bior1fd  1289  3biant1d  1292  equsalhwOLD  1857  equsalOLD  1967  necon2abid  2624  eueq3  3069  sbcel12g  3226  sbceqg  3227  sbcnel12g  3228  sbcne12g  3229  n0moeu  3600  reldisj  3631  r19.3rz  3679  r19.3rzv  3681  r19.9rzv  3682  ordelpss  4569  reusv2lem5  4687  ordsucun  4764  dflim3  4786  dfom2  4806  peano5  4827  rabxp  4873  elrng  5021  iss  5148  elimasni  5190  eliniseg  5192  xpcan  5264  xpcan2  5265  fcnvres  5579  dffv3  5683  funimass4  5736  fndmdif  5793  fneqeql  5797  funimass3  5805  elrnrexdmb  5834  dff4  5842  fconst4  5915  elunirnALT  5959  eqfnov  6135  caoftrn  6298  mpt2xopovel  6430  brtpos  6447  rntpos  6451  opiota  6494  f1ocnvfv3  6544  ordgt0ge1  6700  ondif2  6705  oelim2  6797  omabs  6849  iiner  6935  erinxp  6937  qliftfun  6948  ordunifi  7316  elfi2  7377  elfiun  7393  fifo  7395  noinfep  7570  cantnfrescl  7588  cantnf  7605  rankonidlem  7710  r1pwOLD  7728  pr2nelem  7844  cardalephex  7927  alephinit  7932  dfac5lem4  7963  cflim2  8099  cfsmolem  8106  compssiso  8210  fin1a2lem11  8246  itunisuc  8255  axdclem  8355  brdom6disj  8366  alephreg  8413  fpwwe2lem9  8469  pwfseqlem3  8491  pwfseqlem4  8493  indpi  8740  nqereu  8762  ordpinq  8776  ltanq  8804  ltmnq  8805  suplem2pr  8886  map2psrpr  8941  ssxr  9101  letri3  9116  leltne  9120  ltneg  9484  leneg  9487  suprnub  9927  negiso  9940  infmrgelb  9944  elnnnn0  10219  nn0sub  10226  zrevaddcl  10277  znnsub  10278  znn0sub  10279  prime  10306  eluz2  10450  indstr  10501  eluz2b1  10503  qrevaddcl  10552  rpneg  10597  xrleltne  10694  dfle2  10696  dflt2  10697  xrletri3  10701  supxrleub  10861  infmxrgelb  10869  ixxin  10889  iccid  10917  elicopnf  10956  iccsplit  10985  fzsplit2  11032  fzsn  11050  fzpr  11057  uzsplit  11073  injresinj  11155  om2uzf1oi  11248  lt2sqi  11425  le2sqi  11426  hashsdom  11610  hashf1lem1  11659  fz1isolem  11665  ccatlcan  11733  ccatrcan  11734  cnpart  12000  limsuplt  12228  rlimresb  12314  mertenslem2  12617  sadadd2lem2  12917  saddisjlem  12931  bitsuz  12941  gcddiv  13004  algcvgblem  13023  isprm2lem  13041  isprm3  13043  isprm5  13067  prmreclem5  13243  vdwapun  13297  vdwmc2  13302  ramcl  13352  pwsle  13669  ismre  13770  mreacs  13838  acsfn  13839  iscatd2  13861  cidpropd  13891  oppcsect2  13955  isfunc  14016  setcinv  14200  tosso  14420  ipodrsfi  14544  acsfiindd  14558  imasmnd2  14687  submacs  14720  imasgrp2  14888  issubg  14899  subgacs  14930  eqgval  14944  gaorber  15040  isslw  15197  sylow2alem2  15207  sylow2a  15208  sylow3lem6  15221  efgcpbllemb  15342  prmcyg  15458  gsum2d2lem  15502  gsumcom2  15504  subgdmdprd  15547  dprd2d2  15557  pgpfac1lem2  15588  pgpfac1lem4  15591  imasrng  15680  drngmulne0  15812  lssle0  15981  lssacs  15998  lssats2  16031  lvecvsn0  16136  islpir  16275  isnzr2  16289  zndvds  16785  znleval  16790  znleval2  16791  eltg2b  16979  discld  17108  opnssneib  17134  cldlp  17168  restbas  17176  leordtvallem1  17228  leordtvallem2  17229  ssidcn  17273  cnprest2  17308  lmss  17316  perfcls  17383  cmpfi  17425  1stccnp  17478  subislly  17497  hausmapdom  17516  iskgen3  17534  kgencn  17541  ptpjpre1  17556  xkoccn  17604  txrest  17616  txlm  17633  txkgen  17637  xkopt  17640  xkoinjcn  17672  imasnopn  17675  imasncld  17676  imasncls  17677  qtopcn  17699  kqfeq  17709  isr0  17722  fbfinnfr  17826  trfbas  17829  fbunfip  17854  ufileu  17904  cfinufil  17913  fmid  17945  txflf  17991  fclsrest  18009  alexsubALT  18035  tsmsres  18126  ucnima  18264  fmucndlem  18274  bldisj  18381  xmeter  18416  elbl4  18559  metuel2  18562  restmetu  18570  dscopn  18574  bl2ioo  18776  isphtpc  18972  tchcph  19147  lmmbr2  19165  lmmbrf  19168  iscau2  19183  iscauf  19186  caucfil  19189  metcld  19211  metcld2  19212  bcthlem1  19230  bcthlem4  19233  cldcss2  19296  ovolgelb  19329  ovoliunlem1  19351  ismbfcn  19476  mbfmax  19494  mbfimaopnlem  19500  i1faddlem  19538  i1fmullem  19539  i1fres  19550  i1fpos  19551  itg1climres  19559  xrge0f  19576  itgresr  19623  iblcnlem1  19632  limcun  19735  dvres  19751  mdegmullem  19954  ply1remlem  20038  plyremlem  20174  vieta1  20182  ulmcau  20264  sineq0  20382  coseq1  20383  ang180lem3  20606  cubic  20642  atandm  20669  atandm2  20670  atandm3  20671  rlimcnp  20757  rlimcnp2  20758  vmappw  20852  dchrelbas3  20975  dchrelbas4  20980  dchrsum2  21005  bposlem6  21026  dchrisumlem3  21138  pntleml  21258  nbgrael  21391  nb3gra2nb  21417  nbcusgra  21425  trls  21489  istrl2  21491  is2wlk  21518  0pth  21523  0spth  21524  wlkdvspthlem  21560  0crct  21566  0cycl  21567  eupath2lem2  21653  elghom  21904  nmoolb  22225  nmlno0lem  22247  ubthlem1  22325  ocsh  22738  shle0  22897  eigrei  23290  adjeu  23345  nmoplb  23363  nmfnlb  23380  eleigvec2  23414  nmlnop0iALT  23451  cnlnadjlem5  23527  adjbdln  23539  jplem2  23725  cvbr2  23739  mdsl2bi  23779  chrelat3  23827  ofpreima  24034  funcnvmpt  24036  funcnv5mpt  24037  gtiso  24041  xrdifh  24096  fzsplit3  24103  toslub  24144  tosglb  24145  xrge0tsmsbi  24177  isarchi  24205  unitdivcld  24252  lmxrge0  24290  eldifpr  24345  eldiftp  24346  issibf  24601  dstfrvunirn  24685  ballotlemfc0  24703  ballotlemfcc  24704  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem9  24838  kur14  24855  iscvm  24899  dfpo2  25326  fundmpss  25336  dfon2  25362  elpredg  25392  preduz  25414  tfrALTlem  25490  nofulllem1  25570  nofulllem2  25571  dfbigcup2  25653  dffun10  25667  brimg  25690  funpartfv  25698  dfrdg4  25703  brbtwn2  25748  axsegconlem6  25765  axsegcon  25770  ax5seg  25781  axpasch  25784  axeuclid  25806  axcontlem4  25810  cgr3permute3  25885  segletr  25952  segleantisym  25953  seglelin  25954  mbfposadd  26153  cnambfre  26154  itg2addnclem  26155  itg2addnc  26158  iblabsnclem  26167  fneval  26257  locfindis  26275  neibastop3  26281  eltail  26293  filnetlem4  26300  caures  26356  heiborlem3  26412  heiborlem10  26419  divrngidl  26528  prtlem10  26604  prtlem16  26608  prtlem19  26617  prtex  26619  prter3  26621  isnacs2  26650  rabrenfdioph  26765  expdiophlem1  26982  pw2f1ocnv  26998  pwfi2f1o  27128  numinfctb  27136  dfacbasgrp  27141  lindsmm  27166  islinds3  27172  islindf4  27176  islnr3  27187  subrgacs  27376  sdrgacs  27377  isdomn3  27391  dvconstbi  27419  rfcnpre3  27571  rfcnpre4  27572  stoweidlem59  27675  otthg  27952  f12dfv  27961  el2wlkonotot0  28069  2wot2wont  28083  usg2spthonot1  28087  2spot2iun2spont  28088  vdn1frgrav2  28130  vdgn1frgrav2  28131  usgreg2spot  28170  sbc3org  28327  trsbc  28336  sbcssOLD  28338  bnj919  28842  bnj976  28854  bnj1542  28934  bnj150  28953  bnj151  28954  bnj607  28993  bnj852  28998  bnj873  29001  bnj938  29014  bnj1171  29075  bnj1388  29108  bnj1489  29131  equsalNEW7  29193  islshpat  29500  lcvbr2  29505  lcvbr3  29506  lshpsmreu  29592  isat3  29790  hlrelat5N  29883  islpln5  30017  cdlemblem  30275  paddvaln0N  30283  paddval0  30292  cdlemefrs29bpre1  30879  cdlemefrs29cpre1  30880  cdlemg27b  31178  cdlemg33c  31190  cdlemg33e  31192  diaglbN  31538  cdlemm10N  31601  dicopelval2  31664  dicelval2N  31665  dihopelvalcpre  31731  dihglbcpreN  31783  dih1dimatlem  31812  dihatexv  31821  dvh4dimlem  31926  mapdpglem3  32158  hdmap14lem13  32366  hdmapglem7a  32413

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178