Theorem syl6bi 253

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
syl6bi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
syl6bi.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6bi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 228	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ax12i  1971  sb4a  2480  hbsb2  2482  dfsb2  2493  2eu2  2649  nfabdwOLD  2928  reu6  3723  2reu2  3893  sseq0  4400  disjel  4457  disjpss  4461  preq12b  4852  prneimg  4856  preqsnd  4860  elinti  4960  zfrepclf  5295  dtruALT2  5369  dtruOLD  5442  opth1g  5479  sbcop1  5489  snopeqop  5507  propeqop  5508  otsndisj  5520  otiunsndisj  5521  iunopeqop  5522  po2ne  5605  soasym  5620  elreldm  5935  dfres3  5987  relcnvtrg  6266  relresfld  6276  elpredimg  6316  ordtr2  6409  ordssun  6467  funopg  6583  funimass2  6632  f0dom0  6776  elfv2ex  6938  fveqdmss  7081  eldmrexrnb  7094  fvcofneq  7095  funopsn  7146  funopdmsn  7148  funsndifnop  7149  elunirn  7250  2f1fvneq  7259  oprabidw  7440  oprabid  7441  brfvopab  7466  limuni3  7841  peano5  7884  peano5OLD  7885  op1steq  8019  el2mpocsbcl  8071  bropopvvv  8076  bropfvvvv  8078  f1o2ndf1  8108  frxp  8112  fnwelem  8117  poxp2  8129  suppimacnv  8159  fvn0elsuppb  8166  suppfnss  8174  reldmtpos  8219  rntpos  8224  seqomlem2  8451  oaordi  8546  oa00  8559  oalimcl  8560  omeulem1  8582  nnaordi  8618  ecopovtrn  8814  undifixp  8928  mapdom2  9148  unxpdomlem3  9252  en1eqsn  9274  enp1iOLD  9280  findcard2OLD  9284  infssuni  9343  wdompwdom  9573  preleqg  9610  opthreg  9613  inf3lemd  9622  inf3lem2  9624  inf3lem6  9628  cnfcomlem  9694  cnfcom3  9699  karden  9890  carden2a  9961  alephdom  10076  dfac5lem4  10121  dfac12r  10141  kmlem2  10146  kmlem12  10156  cfslb2n  10263  alephsing  10271  fin23lem30  10337  fin1a2lem6  10400  fin1a2lem13  10407  axcc2lem  10431  domtriomlem  10437  axdc3lem2  10446  axdc4lem  10450  brdom6disj  10527  alephexp1  10574  pwfseq  10659  addnidpi  10896  indpi  10902  nqereu  10924  ltsonq  10964  distrlem5pr  11022  addcanpr  11041  suplem1pr  11047  suplem2pr  11048  ltsrpr  11072  ltsosr  11089  sqgt0sr  11101  leltne  11303  ltnsym  11312  ltlen  11315  eqlei  11324  eqlei2  11325  infm3  12173  nnunb  12468  0mnnnnn0  12504  elnnnn0b  12516  nn0ge2m1nn  12541  nn0le2is012  12626  btwnz  12665  uz11  12847  xrleltne  13124  xltnegi  13195  xnn0lenn0nn0  13224  xnn0xadd0  13226  xmulasslem2  13261  reltxrnmnf  13321  icogelb  13375  iccleub  13379  uznfz  13584  2ffzeq  13622  elfzonlteqm1  13708  elfzo0l  13722  elfznelfzob  13738  elfzr  13745  elfzlmr  13746  injresinjlem  13752  injresinj  13753  fleqceilz  13819  modadd1  13873  modmul1  13889  modirr  13907  addmodlteq  13911  uzrdgfni  13923  fsuppmapnn0fiub0  13958  fsuppmapnn0ub  13960  seqf1o  14009  expnngt1  14204  hashrabsn01  14333  hashrabsn1  14334  hash1snb  14379  hash1n0  14381  hashf1lem2  14417  hash2prde  14431  hash2prd  14436  hash2pwpr  14437  hashle2pr  14438  hashle2prv  14439  hashge2el2dif  14441  hashge2el2difr  14442  fundmge2nop0  14453  ffz0iswrd  14491  ccatrcl1  14544  pfxsuff1eqwrdeq  14649  wrdind  14672  wrd2ind  14673  swrdccatin1  14675  swrdccat3blem  14689  2cshwcshw  14776  cshwcsh2id  14779  cshimadifsn  14780  2swrd2eqwrdeq  14904  wwlktovf  14907  wwlktovfo  14909  s3sndisj  14914  s3iunsndisj  14915  relexpindlem  15010  rexico  15300  lo1le  15598  fsum2dlem  15716  ntrivcvg  15843  fprodss  15892  fprod2dlem  15924  0dvds  16220  mod2eq1n2dvds  16290  opoe  16306  omoe  16307  opeo  16308  omeo  16309  m1exp1  16319  nn0enne  16320  nn0o1gt2  16324  gcdneg  16463  dfgcd2  16488  algcvga  16516  eucalglt  16522  lcmf  16570  coprmdvds  16590  divgcdcoprmex  16603  cncongr1  16604  prm2orodd  16628  prm23lt5  16747  pockthi  16840  prmreclem5  16853  ramtcl2  16944  cshwrepswhash1  17036  f1ocpbl  17471  f1ovscpbl  17472  f1olecpbl  17473  monhom  17682  epihom  17689  inveq  17721  invcoisoid  17739  isocoinvid  17740  ciclcl  17749  cicrcl  17750  isinitoi  17949  istermoi  17950  2initoinv  17960  2termoinv  17967  setciso  18041  embedsetcestrclem  18109  ipopos  18489  gsumval2a  18604  ismnddef  18627  dfgrp2e  18848  symg2bas  19260  snsymgefmndeq  19262  symgvalstruct  19264  symgvalstructOLD  19265  symgfix2  19284  gsmsymgreq  19300  pmtrdifellem4  19347  mndodcongi  19411  pj1eu  19564  cycsubmcmn  19757  dprd2da  19912  0ring01eq  20304  lmodfopnelem1  20508  lspdisjb  20739  lspsnsubn0  20753  obs2ss  21284  psrbaglefiOLD  21486  mamufacex  21891  mat0dim0  21969  mat0dimid  21970  mat0dimscm  21971  dmatmat  21996  scmatmat  22011  mat1scmat  22041  1mavmul  22050  mavmulsolcl  22053  gsummatr01  22161  cpmatpmat  22212  cpmadugsumlemF  22378  tg2  22468  tgcl  22472  neii1  22610  neii2  22612  neindisj2  22627  perfopn  22689  ordtbas2  22695  pnfnei  22724  mnfnei  22725  llyidm  22992  txlm  23152  qtopuni  23206  tgqtop  23216  isfild  23362  snfil  23368  fbunfip  23373  fgss2  23378  fmco  23465  fbflim2  23481  cnpflf2  23504  fcfelbas  23540  fcfneii  23541  alexsubALTlem2  23552  alexsubALT  23555  tgpconncompeqg  23616  tsmscl  23639  tngngpim  24176  tgioo  24312  xrsmopn  24328  iccntr  24337  reconnlem2  24343  addcnlem  24380  htpycn  24489  phtpyhtpy  24498  pi1blem  24555  fgcfil  24788  ioombl1lem4  25078  dyadmbl  25117  itg2gt0  25278  ditgneg  25374  dvivthlem1  25525  coeeq2  25756  aannenlem2  25842  sineq0  26033  efif1o  26055  xrlimcnp  26473  vmacl  26622  efvmacl  26624  vmalelog  26708  dchrelbasd  26742  lgsqr  26854  lgsqrmodndvds  26856  gausslemma2dlem0i  26867  2lgslem2  26898  2lgs  26910  2lgsoddprmlem3  26917  2sqnn  26942  2sqreultlem  26950  2sqreultblem  26951  2sqreunnltlem  26953  2sqreunnltblem  26954  sltintdifex  27164  sltres  27165  nosepnelem  27182  nolt02o  27198  negsprop  27512  mulsprop  27589  elntg2  28274  uhgr0vb  28363  umgrupgr  28394  umgrnloopv  28397  umgredgprv  28398  umgrislfupgrlem  28413  umgredg  28429  uspgrushgr  28466  uspgrupgr  28467  usgruspgr  28469  usgredgprvALT  28483  usgrnloopvALT  28489  uhgr2edg  28496  edg0usgr  28541  egrsubgr  28565  0uhgrsubgr  28567  uhgrspansubgrlem  28578  nbuhgr  28631  cusgrsize2inds  28741  cusgrfilem2  28744  vtxdg0v  28761  1loopgrnb0  28790  vtxdginducedm1lem4  28830  wlkvtxeledg  28912  wlkeq  28922  wlkl1loop  28926  wlk1walk  28927  upgrwlkedg  28930  uspgr2wlkeq  28934  wlkv0  28939  wlkonl1iedg  28953  wlkon2n0  28954  wlkp1lem8  28968  wlkp1  28969  lfgrwlkprop  28975  lfgrwlknloop  28977  2pthnloop  29019  upgrwlkdvde  29025  spthonepeq  29040  uhgrwkspthlem2  29042  usgr2wlkneq  29044  usgr2trlncl  29048  usgr2trlspth  29049  pthdlem2lem  29055  clwlkcompbp  29070  uspgrn2crct  29093  wwlks  29120  wwlknbp  29127  0enwwlksnge1  29149  wwlkswwlksn  29150  wlklnwwlkln1  29153  wwlksnextproplem3  29196  wwlksnextprop  29197  wspthsnonn0vne  29202  wspn0  29209  2pthon3v  29228  umgr2adedgspth  29233  rusgr0edg  29258  clwwlkccat  29274  clwlkclwwlklem2fv2  29280  clwlkclwwlklem2a4  29281  clwlkclwwlklem2  29284  clwlkclwwlkflem  29288  clwwlknp  29321  clwwlkwwlksb  29338  clwwlkext2edg  29340  erclwwlkneqlen  29352  hashecclwwlkn1  29361  umgrhashecclwwlk  29362  clwwlknonwwlknonb  29390  upgr1wlkdlem1  29429  upgr3v3e3cycl  29464  uhgr3cyclexlem  29465  1conngr  29478  conngrv2edg  29479  eupth2lem3lem4  29515  eulercrct  29526  isfrgr  29544  frgr3vlem2  29558  1to2vfriswmgr  29563  1to3vfriswmgr  29564  frgrncvvdeqlem9  29591  frgrwopreg  29607  frgr2wwlkeqm  29615  2wspmdisj  29621  numclwwlk1lem2f  29639  frgrreggt1  29677  frgrregord013  29679  frgrregord13  29680  l2p  29763  nmlno0lem  30077  normgt0  30411  ocin  30580  nmlnop0iALT  31279  nmopun  31298  cvpss  31569  cvnbtwn  31570  atcvati  31670  mdsymlem6  31692  iunrnmptss  31828  wrdt2ind  32148  irngssv  32783  issgon  33152  mbfmcnt  33298  ballotlemfc0  33522  ballotlemfcc  33523  satfv0  34380  satfv0fun  34393  fmla1  34409  gonarlem  34416  gonar  34417  goalrlem  34418  goalr  34419  fmla0disjsuc  34420  satffunlem  34423  satffunlem1lem1  34424  satffunlem2lem1  34426  satfun  34433  satfv0fvfmla0  34435  sategoelfv  34442  mthmblem  34602  pprodss4v  34887  funpartfun  34946  funpartfv  34948  5segofs  35009  btwnxfr  35059  brofs2  35080  brifs2  35081  btwnconn1  35104  segleantisym  35118  broutsideof2  35125  outsidene1  35126  outsidene2  35127  funray  35143  lineunray  35150  cldbnd  35259  bj-imdirval3  36113  topdifinffinlem  36276  isbasisrelowllem1  36284  isbasisrelowllem2  36285  relowlpssretop  36293  inunissunidif  36304  pibt2  36346  matunitlindf  36534  poimir  36569  volsupnfl  36581  itg2addnclem  36587  cover2  36631  sdclem2  36658  fdc  36661  sstotbnd3  36692  heibor1  36726  clmgmOLD  36767  smgrpmgm  36780  smgrpassOLD  36781  dvrunz  36870  0rngo  36943  mopickr  37280  lsatcvat  37968  lshpkrex  38036  cmtbr3N  38172  atn0  38226  atnle  38235  cvlsupr4  38263  cvlsupr5  38264  cvlsupr6  38265  cvrval4N  38333  cvratlem  38340  2llnjN  38486  2lplnj  38539  linepsubN  38671  elpaddatiN  38724  elpcliN  38812  pclcmpatN  38820  ldilval  39032  ltrnu  39040  cdleme18d  39214  tendotp  39680  tendof  39682  tendovalco  39684  diatrl  39963  diaintclN  39977  dvheveccl  40031  dibintclN  40086  dihord6apre  40175  dihmeetlem1N  40209  dihpN  40255  dihintcl  40263  dochkrshp4  40308  oexpreposd  41260  pw2f1ocnv  41824  iocinico  42009  onsucf1olem  42068  succlg  42126  oacl2g  42128  omabs2  42130  omcl2  42131  naddcnfcom  42164  naddcnfass  42167  safesnsupfidom1o  42216  infordmin  42331  pr2cv  42347  expgrowthi  43140  iotavalsb  43240  bi23imp1  43304  ioogtlb  44256  iocgtlb  44263  iocleub  44264  icoltub  44269  iooltub  44271  stoweidlem31  44795  oppr  45788  funressnfv  45801  fsetsniunop  45807  fsetsnf1  45810  eu2ndop1stv  45881  afvelrnb0  45920  otiunsndisjX  46035  el1fzopredsuc  46081  fzoopth  46083  2ffzoeq  46084  uniimaprimaeqfv  46098  elsetpreimafveqfv  46108  iccpartimp  46133  iccpartrn  46146  iccpartf  46147  iccpartnel  46154  fargshiftf  46156  fargshiftfo  46158  ichnfimlem  46179  ichnfim  46180  ichreuopeq  46189  sprel  46200  sprsymrelfvlem  46206  sprsymrelfolem2  46209  prproropf1olem4  46222  prprelb  46232  poprelb  46240  fmtnofac1  46286  prmdvdsfmtnof1lem2  46301  31prm  46313  lighneallem3  46323  nn0o1gt2ALTV  46410  nn0oALTV  46412  odd2prm2  46434  mogoldbblem  46436  fpprbasnn  46445  fpprnn  46446  sbgoldbaltlem1  46495  nnsum3primesle9  46510  bgoldbtbndlem1  46521  bgoldbtbndlem2  46522  isomuspgrlem2d  46547  upwlkbprop  46564  mgmpropd  46593  clcllaw  46649  intop  46661  assintop  46667  assintopcllaw  46670  rngimf1o  46751  rngimrnghm  46752  c0snmgmhm  46761  rngqiprngfulem2  46845  elrngchom  46914  rnghmsubcsetclem1  46921  rnghmsubcsetclem2  46922  rngcid  46925  rngcinv  46927  rngciso  46928  elrngchomALTV  46932  rngccatidALTV  46935  rngcinvALTV  46939  rngcisoALTV  46940  funcrngcsetcALT  46945  zrinitorngc  46946  zrtermorngc  46947  elringchom  46960  rhmsubcsetclem1  46967  rhmsubcsetclem2  46968  ringcid  46971  rhmsubcrngclem1  46973  rhmsubcrngclem2  46974  ringciso  46979  funcringcsetcALTV2lem7  46988  elringchomALTV  46995  ringccatidALTV  46998  ringcisoALTV  47003  funcringcsetclem7ALTV  47011  irinitoringc  47015  zrtermoringc  47016  rhmsubclem3  47034  rhmsubclem4  47035  rhmsubcALTVlem3  47052  rhmsubcALTVlem4  47053  ztprmneprm  47071  suppmptcfin  47103  linccl  47143  linc1  47154  lincolss  47163  ldepspr  47202  nn0sumshdiglem1  47355  0aryfvalelfv  47369  rrxlines  47467  rrxsphere  47482  itsclc0yqsol  47498  itschlc0xyqsol1  47500  fdomne0  47564  f002  47568  fvconstr2  47572  fullthinc  47714