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  313  mtt  339  nbn2  345  rbaibr  905  3bior1fd  1334  3biant1d  1337  clelab  2601  necon2abidOLD  2712  eueq3  3274  n0moeu  3807  sbcel12  3832  sbcel12gOLD  3833  sbceqg  3834  sbcne12  3836  reldisj  3873  raldifeq  3920  r19.3rz  3923  r19.3rzv  3925  r19.9rzv  3926  eldifpr  4049  eldiftp  4075  reusv2lem5  4661  otthg  4739  ordelpss  4915  rabxp  5045  elrng  5204  iss  5331  elimasni  5374  eliniseg  5376  xpcan  5450  xpcan2  5451  fcnvres  5768  dffv3  5868  funimass4  5924  fndmdif  5992  fneqeql  5996  funimass3  6004  elrnrexdmb  6037  dff4  6046  fnsnb  6091  fconst4  6137  elunirn  6164  f12dfv  6180  riota1  6276  riota2df  6278  f1ocnvfv3  6292  eqfnov  6407  elrnmpt2res  6415  caoftrn  6574  ordsucun  6659  dflim3  6681  dfom2  6701  peano5  6722  opiota  6858  suppssr  6949  mpt2xopovel  6966  brtpos  6982  rntpos  6986  ordgt0ge1  7165  ondif2  7170  oelim2  7262  omabs  7314  iiner  7401  erinxp  7403  qliftfun  7414  ordunifi  7788  elfi2  7892  elfiun  7908  fifo  7910  noinfep  8093  cantnflem1  8125  cantnf  8129  cantnfOLD  8151  rankonidlem  8263  r1pwALT  8281  pr2nelem  8399  cardalephex  8488  alephinit  8493  dfac5lem4  8524  cflim2  8660  cfsmolem  8667  compssiso  8771  fin1a2lem11  8807  itunisuc  8816  axdclem  8916  brdom6disj  8927  alephreg  8974  fpwwe2lem9  9033  pwfseqlem3  9055  pwfseqlem4  9057  indpi  9302  nqereu  9324  ordpinq  9338  ltanq  9366  ltmnq  9367  suplem2pr  9448  map2psrpr  9504  ssxr  9671  letri3  9687  leltne  9691  ltneg  10073  leneg  10076  suprnub  10526  negiso  10539  infmrgelb  10543  elnnnn0  10860  nn0sub  10867  zrevaddcl  10930  znnsub  10931  znn0sub  10932  prime  10964  eluz2  11112  indstr  11175  eluz2b1  11178  qrevaddcl  11229  rpneg  11274  xrleltne  11376  dfle2  11378  dflt2  11379  xrletri3  11383  supxrleub  11543  infmxrgelb  11551  ixxin  11571  iccid  11599  elicopnf  11645  iccsplit  11678  fzsplit2  11735  fzsn  11751  fzpr  11761  uzsplit  11776  injresinj  11929  om2uzf1oi  12067  lt2sqi  12259  le2sqi  12260  hashsdom  12452  hashf1lem1  12508  fz1isolem  12514  ccatlcan  12709  ccatrcan  12710  2swrd2eqwrdeq  12903  cnpart  13085  limsuplt  13314  rlimresb  13400  mertenslem2  13706  fprod2dlem  13796  sadadd2lem2  14112  saddisjlem  14126  bitsuz  14136  gcddiv  14199  algcvgblem  14218  isprm2lem  14236  isprm3  14238  isprm5  14265  prmreclem5  14450  vdwapun  14504  vdwmc2  14509  ramcl  14559  pwsle  14909  ismre  15007  mreacs  15075  acsfn  15076  iscatd2  15098  cidpropd  15126  dfiso2  15188  oppcsect2  15195  isfunc  15280  setcinv  15496  lubeldm  15738  lubval  15741  glbeldm  15751  glbval  15754  tosso  15793  ipodrsfi  15920  acsfiindd  15934  imasmnd2  16084  submacs  16123  imasgrp2  16312  issubg  16328  resgrpisgrp  16349  subgacs  16363  eqgval  16377  gaorber  16473  symgfix2  16568  psgnran  16667  isslw  16755  sylow2alem2  16765  sylow2a  16766  sylow3lem6  16779  efgcpbllemb  16900  prmcyg  17023  gsum2d2lem  17128  gsumcom2  17130  subgdmdprd  17208  dprd2d2  17220  pgpfac1lem2  17253  pgpfac1lem4  17256  imasring  17395  drngmulne0  17545  lssle0  17723  lssacs  17740  lssats2  17773  lvecvsn0  17882  islpir  18024  isnzr2  18038  zndvds  18715  znleval  18720  znleval2  18721  lindsmm  18990  islinds3  18996  islindf4  19000  eltg2b  19587  discld  19717  opnssneib  19743  cldlp  19778  restbas  19786  leordtvallem1  19838  leordtvallem2  19839  ssidcn  19883  cnprest2  19918  lmss  19926  perfcls  19993  cmpfi  20035  1stccnp  20089  subislly  20108  hausmapdom  20127  locfindis  20157  iskgen3  20176  kgencn  20183  ptpjpre1  20198  xkoccn  20246  txrest  20258  txlm  20275  txkgen  20279  xkopt  20282  xkoinjcn  20314  imasnopn  20317  imasncld  20318  imasncls  20319  qtopcn  20341  kqfeq  20351  isr0  20364  fbfinnfr  20468  trfbas  20471  fbunfip  20496  ufileu  20546  cfinufil  20555  fmid  20587  txflf  20633  fclsrest  20651  alexsubALT  20677  tsmsresOLD  20771  tsmsres  20772  ucnima  20910  fmucndlem  20920  bldisj  21027  xmeter  21062  elbl4  21205  restmetu  21216  dscopn  21220  bl2ioo  21423  isphtpc  21620  tchcph  21806  lmmbr2  21824  lmmbrf  21827  iscau2  21842  iscauf  21845  caucfil  21848  metcld  21870  metcld2  21871  bcthlem1  21889  bcthlem4  21892  cldcss2  21983  ovolgelb  22017  ovoliunlem1  22039  ismbfcn  22164  mbfmax  22182  mbfimaopnlem  22188  i1faddlem  22226  i1fmullem  22227  i1fres  22238  i1fpos  22239  itg1climres  22247  xrge0f  22264  itgresr  22311  iblcnlem1  22320  limcun  22425  dvres  22441  mdegmullem  22604  ply1remlem  22689  plyremlem  22826  vieta1  22834  ulmcau  22916  sineq0  23040  coseq1  23041  ang180lem3  23269  cubic  23306  atandm  23333  atandm2  23334  atandm3  23335  rlimcnp  23421  rlimcnp2  23422  vmappw  23516  dchrelbas3  23639  dchrelbas4  23644  dchrsum2  23669  bposlem6  23690  dchrisumlem3  23802  pntleml  23922  lnrot2  24130  islnopp  24239  islmib  24279  brbtwn2  24335  axsegconlem6  24352  axsegcon  24357  ax5seg  24368  axpasch  24371  axeuclid  24393  axcontlem4  24397  usgrac  24478  elusuhgra  24495  nbgrael  24553  nb3gra2nb  24582  nbcusgra  24590  wlkcomp  24652  trls  24665  istrl2  24667  is2wlk  24694  0pth  24699  0spth  24700  wlkdvspthlem  24736  0crct  24753  0cycl  24754  clwlkcomp  24890  clwlkisclwwlklem0  24915  clwlkisclwwlk  24916  el2wlkonotot0  24999  2wot2wont  25013  usg2spthonot1  25017  2spot2iun2spont  25018  isrusgra  25054  isrusgusrgcl  25060  isrusgrac  25062  0eusgraiff0rgracl  25068  rusgranumwlks  25083  eupath2lem2  25105  vdn1frgrav2  25152  vdgn1frgrav2  25153  usgreg2spot  25194  numclwwlkovgel  25215  elghomOLD  25492  nmoolb  25813  nmlno0lem  25835  ubthlem1  25913  ocsh  26328  shle0  26487  eigrei  26880  adjeu  26935  nmoplb  26953  nmfnlb  26970  eleigvec2  27004  nmlnop0iALT  27041  cnlnadjlem5  27117  adjbdln  27129  jplem2  27315  cvbr2  27329  mdsl2bi  27369  chrelat3  27417  disjunsn  27593  ofpreima  27661  funcnvmpt  27664  funcnv5mpt  27665  dfcnv2  27672  gtiso  27674  fpwrelmap  27713  xrdifh  27751  fzsplit3  27759  toslublem  27815  tosglblem  27817  isarchi  27886  xrge0tsmsbi  27937  unitdivcld  28044  lmxrge0  28095  isrrext  28142  issibf  28472  eulerpartlemr  28510  eulerpartlemmf  28511  eulerpartlemn  28517  dstfrvunirn  28610  ballotlemfc0  28628  ballotlemfcc  28629  subfacp1lem3  28823  subfacp1lem5  28825  erdszelem9  28840  kur14  28857  iscvm  28901  mclsax  29126  dfpo2  29402  fundmpss  29414  opelco3  29425  dfon2  29441  elpredg  29475  preduz  29497  nofulllem1  29679  nofulllem2  29680  dfbigcup2  29754  sscoid  29768  funpartfv  29800  dfrdg4  29805  cgr3permute3  29902  segletr  29969  segleantisym  29970  seglelin  29971  cos2h  30251  tan2h  30252  mbfposadd  30267  cnambfre  30268  dvtanlem  30269  itg2addnclem  30271  itg2addnc  30274  iblabsnclem  30283  ftc1anclem1  30295  ftc1anclem5  30299  fneval  30375  neibastop3  30385  eltail  30397  filnetlem4  30404  caures  30458  heiborlem3  30514  heiborlem10  30521  divrngidl  30630  prtlem10  30811  prtlem16  30815  prtlem19  30824  prtex  30826  prter3  30828  isnacs2  30843  rabrenfdioph  30952  expdiophlem1  31167  pw2f1ocnv  31183  pwfi2f1o  31248  numinfctb  31256  dfacbasgrp  31261  islnr3  31268  subrgacs  31353  sdrgacs  31354  isdomn3  31368  hashnzfzclim  31431  dvconstbi  31443  rfcnpre3  31611  rfcnpre4  31612  unima  31644  cncfshift  31879  stoweidlem59  32044  prelpw  32563  uhgrasiz  32656  isfusgracl  32688  isfusgraclALT  32690  fusgraimpclALT2  32693  usgfis  32708  usgfisALT  32712  submgmacs  32754  ismhm0  32755  iscmgmALT  32810  iscsgrpALT  32812  isrnghmmul  32843  sbc3orgOLD  33446  sbcssOLD  33456  bnj919  33968  bnj976  33979  bnj1542  34058  bnj150  34077  bnj151  34078  bnj607  34117  bnj852  34122  bnj873  34125  bnj938  34138  bnj1171  34199  bnj1388  34232  bnj1489  34255  bj-hbntbi  34401  bj-sbceqgALT  34612  islshpat  34885  lcvbr2  34890  lcvbr3  34891  lshpsmreu  34977  isat3  35175  hlrelat5N  35268  islpln5  35402  cdlemblem  35660  paddvaln0N  35668  paddval0  35677  cdlemefrs29bpre1  36266  cdlemefrs29cpre1  36267  cdlemg27b  36565  cdlemg33c  36577  cdlemg33e  36579  diaglbN  36925  cdlemm10N  36988  dicopelval2  37051  dicelval2N  37052  dihopelvalcpre  37118  dihglbcpreN  37170  dih1dimatlem  37199  dihatexv  37208  dvh4dimlem  37313  mapdpglem3  37545  hdmap14lem13  37753  hdmapglem7a  37800  trclfvcotr  37969  dfhe3  37989