Theorem syl6bi 256

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 232	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ax12i  1974  sb3OLD  2481  sb1OLD  2482  sb4a  2484  hbsb2  2486  dfsb2  2497  2eu2  2655  nfabdwOLD  2923  reu6  3625  2reu2  3789  sseq0  4288  disjel  4346  disjpss  4350  preq12b  4736  prneimg  4740  preqsnd  4744  elinti  4845  zfrepclf  5162  dtru  5237  opth1g  5336  sbcop1  5345  snopeqop  5363  propeqop  5364  otsndisj  5376  otiunsndisj  5377  iunopeqop  5378  po2ne  5458  soasym  5473  elreldm  5778  dfres3  5830  relcnvtrg  6099  relresfld  6108  ordtr2  6216  ordssun  6271  funopg  6373  funimass2  6422  f0dom0  6562  elfv2ex  6715  fveqdmss  6856  eldmrexrnb  6868  fvcofneq  6869  funopsn  6920  funopdmsn  6922  funsndifnop  6923  elunirn  7021  2f1fvneq  7029  oprabidw  7201  oprabid  7202  brfvopab  7225  limuni3  7586  peano5  7624  peano5OLD  7625  op1steq  7758  el2mpocsbcl  7806  bropopvvv  7811  bropfvvvv  7813  f1o2ndf1  7844  frxp  7846  fnwelem  7851  suppimacnv  7869  fvn0elsuppb  7876  suppfnss  7884  reldmtpos  7929  rntpos  7934  seqomlem2  8116  oaordi  8203  oa00  8216  oalimcl  8217  omeulem1  8239  nnaordi  8275  ecopovtrn  8431  undifixp  8544  mapdom2  8738  unxpdomlem3  8803  enp1i  8830  findcard2OLD  8834  infssuni  8888  wdompwdom  9115  preleqg  9151  opthreg  9154  inf3lemd  9163  inf3lem2  9165  inf3lem6  9169  cnfcomlem  9235  cnfcom3  9240  karden  9397  carden2a  9468  alephdom  9581  dfac5lem4  9626  dfac12r  9646  kmlem2  9651  kmlem12  9661  cfslb2n  9768  alephsing  9776  fin23lem30  9842  fin1a2lem6  9905  fin1a2lem13  9912  axcc2lem  9936  domtriomlem  9942  axdc3lem2  9951  axdc4lem  9955  brdom6disj  10032  alephexp1  10079  pwfseq  10164  addnidpi  10401  indpi  10407  nqereu  10429  ltsonq  10469  distrlem5pr  10527  addcanpr  10546  suplem1pr  10552  suplem2pr  10553  ltsrpr  10577  ltsosr  10594  sqgt0sr  10606  leltne  10808  ltnsym  10816  ltlen  10819  eqlei  10828  eqlei2  10829  infm3  11677  nnunb  11972  0mnnnnn0  12008  elnnnn0b  12020  nn0ge2m1nn  12045  nn0le2is012  12127  btwnz  12165  uz11  12349  xrleltne  12621  xltnegi  12692  xnn0lenn0nn0  12721  xnn0xadd0  12723  xmulasslem2  12758  reltxrnmnf  12818  icogelb  12872  iccleub  12876  uznfz  13081  2ffzeq  13119  elfzonlteqm1  13204  elfzo0l  13218  elfznelfzob  13234  elfzr  13241  elfzlmr  13242  injresinjlem  13248  injresinj  13249  fleqceilz  13313  modadd1  13367  modmul1  13383  modirr  13401  addmodlteq  13405  uzrdgfni  13417  fsuppmapnn0fiub0  13452  fsuppmapnn0ub  13454  seqf1o  13503  expnngt1  13694  hashrabsn01  13826  hashrabsn1  13827  hash1snb  13872  hash1n0  13874  hashf1lem2  13908  hash2prde  13922  hash2prd  13927  hash2pwpr  13928  hashle2pr  13929  hashle2prv  13930  hashge2el2dif  13932  hashge2el2difr  13933  fundmge2nop0  13944  ffz0iswrd  13982  ccatrcl1  14037  pfxsuff1eqwrdeq  14150  wrdind  14173  wrd2ind  14174  swrdccatin1  14176  swrdccat3blem  14190  2cshwcshw  14276  cshwcsh2id  14279  cshimadifsn  14280  2swrd2eqwrdeq  14404  wwlktovf  14409  wwlktovfo  14411  s3sndisj  14416  s3iunsndisj  14417  relexpindlem  14512  rexico  14803  lo1le  15101  fsum2dlem  15218  ntrivcvg  15345  fprodss  15394  fprod2dlem  15426  0dvds  15722  mod2eq1n2dvds  15792  opoe  15808  omoe  15809  opeo  15810  omeo  15811  m1exp1  15821  nn0enne  15822  nn0o1gt2  15826  gcdneg  15965  dfgcd2  15990  algcvga  16020  eucalglt  16026  lcmf  16074  coprmdvds  16094  divgcdcoprmex  16107  cncongr1  16108  prm2orodd  16132  prm23lt5  16251  pockthi  16343  prmreclem5  16356  ramtcl2  16447  cshwrepswhash1  16539  f1ocpbl  16901  f1ovscpbl  16902  f1olecpbl  16903  monhom  17110  epihom  17117  inveq  17149  invcoisoid  17167  isocoinvid  17168  ciclcl  17177  cicrcl  17178  isinitoi  17371  istermoi  17372  2initoinv  17382  2termoinv  17389  setciso  17463  embedsetcestrclem  17523  ipopos  17886  gsumval2a  18011  ismnddef  18029  dfgrp2e  18247  symg2bas  18639  snsymgefmndeq  18641  symgvalstruct  18643  symgfix2  18662  gsmsymgreq  18678  pmtrdifellem4  18725  mndodcongi  18789  pj1eu  18940  cycsubmcmn  19127  dprd2da  19283  rimf1o  19608  rimrhm  19609  brric2  19619  lmodfopnelem1  19789  lspdisjb  20017  lspsnsubn0  20031  0ring01eq  20163  obs2ss  20545  psrbaglefiOLD  20746  mamufacex  21142  mat0dim0  21218  mat0dimid  21219  mat0dimscm  21220  dmatmat  21245  scmatmat  21260  mat1scmat  21290  1mavmul  21299  mavmulsolcl  21302  gsummatr01  21410  cpmatpmat  21461  cpmadugsumlemF  21627  tg2  21716  tgcl  21720  neii1  21857  neii2  21859  neindisj2  21874  perfopn  21936  ordtbas2  21942  pnfnei  21971  mnfnei  21972  llyidm  22239  txlm  22399  qtopuni  22453  tgqtop  22463  isfild  22609  snfil  22615  fbunfip  22620  fgss2  22625  fmco  22712  fbflim2  22728  cnpflf2  22751  fcfelbas  22787  fcfneii  22788  alexsubALTlem2  22799  alexsubALT  22802  tgpconncompeqg  22863  tsmscl  22886  tngngpim  23412  tgioo  23548  xrsmopn  23564  iccntr  23573  reconnlem2  23579  addcnlem  23616  htpycn  23725  phtpyhtpy  23734  pi1blem  23791  fgcfil  24023  ioombl1lem4  24313  dyadmbl  24352  itg2gt0  24513  ditgneg  24609  dvivthlem1  24760  coeeq2  24991  aannenlem2  25077  sineq0  25268  efif1o  25290  xrlimcnp  25706  vmacl  25855  efvmacl  25857  vmalelog  25941  dchrelbasd  25975  lgsqr  26087  lgsqrmodndvds  26089  gausslemma2dlem0i  26100  2lgslem2  26131  2lgs  26143  2lgsoddprmlem3  26150  2sqnn  26175  2sqreultlem  26183  2sqreultblem  26184  2sqreunnltlem  26186  2sqreunnltblem  26187  elntg2  26931  uhgr0vb  27017  umgrupgr  27048  umgrnloopv  27051  umgredgprv  27052  umgrislfupgrlem  27067  umgredg  27083  uspgrushgr  27120  uspgrupgr  27121  usgruspgr  27123  usgredgprvALT  27137  usgrnloopvALT  27143  uhgr2edg  27150  edg0usgr  27195  egrsubgr  27219  0uhgrsubgr  27221  uhgrspansubgrlem  27232  nbuhgr  27285  cusgrsize2inds  27395  cusgrfilem2  27398  vtxdg0v  27415  1loopgrnb0  27444  vtxdginducedm1lem4  27484  wlkvtxeledg  27565  wlkeq  27575  wlkl1loop  27579  wlk1walk  27580  upgrwlkedg  27583  uspgr2wlkeq  27587  wlkv0  27592  wlkonl1iedg  27607  wlkon2n0  27608  wlkp1lem8  27622  wlkp1  27623  lfgrwlkprop  27629  lfgrwlknloop  27631  2pthnloop  27672  upgrwlkdvde  27678  spthonepeq  27693  uhgrwkspthlem2  27695  usgr2wlkneq  27697  usgr2trlncl  27701  usgr2trlspth  27702  pthdlem2lem  27708  clwlkcompbp  27723  uspgrn2crct  27746  wwlks  27773  wwlknbp  27780  0enwwlksnge1  27802  wwlkswwlksn  27803  wlklnwwlkln1  27806  wwlksnextproplem3  27849  wwlksnextprop  27850  wspthsnonn0vne  27855  wspn0  27862  2pthon3v  27881  umgr2adedgspth  27886  rusgr0edg  27911  clwwlkccat  27927  clwlkclwwlklem2fv2  27933  clwlkclwwlklem2a4  27934  clwlkclwwlklem2  27937  clwlkclwwlkflem  27941  clwwlknp  27974  clwwlkwwlksb  27991  clwwlkext2edg  27993  erclwwlkneqlen  28005  hashecclwwlkn1  28014  umgrhashecclwwlk  28015  clwwlknonwwlknonb  28043  upgr1wlkdlem1  28082  upgr3v3e3cycl  28117  uhgr3cyclexlem  28118  1conngr  28131  conngrv2edg  28132  eupth2lem3lem4  28168  eulercrct  28179  isfrgr  28197  frgr3vlem2  28211  1to2vfriswmgr  28216  1to3vfriswmgr  28217  frgrncvvdeqlem9  28244  frgrwopreg  28260  frgr2wwlkeqm  28268  2wspmdisj  28274  numclwwlk1lem2f  28292  frgrreggt1  28330  frgrregord013  28332  frgrregord13  28333  l2p  28414  nmlno0lem  28728  normgt0  29062  ocin  29231  nmlnop0iALT  29930  nmopun  29949  cvpss  30220  cvnbtwn  30221  atcvati  30321  mdsymlem6  30343  iunrnmptss  30479  wrdt2ind  30800  issgon  31661  mbfmcnt  31805  ballotlemfc0  32029  ballotlemfcc  32030  satfv0  32891  satfv0fun  32904  fmla1  32920  gonarlem  32927  gonar  32928  goalrlem  32929  goalr  32930  fmla0disjsuc  32931  satffunlem  32934  satffunlem1lem1  32935  satffunlem2lem1  32937  satfun  32944  satfv0fvfmla0  32946  sategoelfv  32953  mthmblem  33113  poxp2  33401  sltintdifex  33505  sltres  33506  nosepnelem  33523  nolt02o  33539  pprodss4v  33824  funpartfun  33883  funpartfv  33885  5segofs  33946  btwnxfr  33996  brofs2  34017  brifs2  34018  btwnconn1  34041  segleantisym  34055  broutsideof2  34062  outsidene1  34063  outsidene2  34064  funray  34080  lineunray  34087  cldbnd  34153  bj-dtru  34630  bj-imdirval3  34976  topdifinffinlem  35141  isbasisrelowllem1  35149  isbasisrelowllem2  35150  relowlpssretop  35158  inunissunidif  35169  pibt2  35211  matunitlindf  35398  poimir  35433  volsupnfl  35445  itg2addnclem  35451  cover2  35495  sdclem2  35523  fdc  35526  sstotbnd3  35557  heibor1  35591  clmgmOLD  35632  smgrpmgm  35645  smgrpassOLD  35646  dvrunz  35735  0rngo  35808  lsatcvat  36687  lshpkrex  36755  cmtbr3N  36891  atn0  36945  atnle  36954  cvlsupr4  36982  cvlsupr5  36983  cvlsupr6  36984  cvrval4N  37051  cvratlem  37058  2llnjN  37204  2lplnj  37257  linepsubN  37389  elpaddatiN  37442  elpcliN  37530  pclcmpatN  37538  ldilval  37750  ltrnu  37758  cdleme18d  37932  tendotp  38398  tendof  38400  tendovalco  38402  diatrl  38681  diaintclN  38695  dvheveccl  38749  dibintclN  38804  dihord6apre  38893  dihmeetlem1N  38927  dihpN  38973  dihintcl  38981  dochkrshp4  39026  oexpreposd  39897  pw2f1ocnv  40431  iocinico  40615  infordmin  40693  pr2cv  40700  expgrowthi  41489  iotavalsb  41589  bi23imp1  41653  ioogtlb  42573  iocgtlb  42580  iocleub  42581  icoltub  42586  iooltub  42588  stoweidlem31  43114  oppr  44063  funressnfv  44076  fsetsniunop  44081  fsetsnf1  44084  eu2ndop1stv  44150  afvelrnb0  44189  otiunsndisjX  44304  el1fzopredsuc  44351  fzoopth  44353  2ffzoeq  44354  uniimaprimaeqfv  44368  elsetpreimafveqfv  44378  iccpartimp  44403  iccpartrn  44416  iccpartf  44417  iccpartnel  44424  fargshiftf  44426  fargshiftfo  44428  ichnfimlem  44449  ichnfim  44450  ichreuopeq  44459  sprel  44470  sprsymrelfvlem  44476  sprsymrelfolem2  44479  prproropf1olem4  44492  prprelb  44502  poprelb  44510  fmtnofac1  44556  prmdvdsfmtnof1lem2  44571  31prm  44583  lighneallem3  44593  nn0o1gt2ALTV  44680  nn0oALTV  44682  odd2prm2  44704  mogoldbblem  44706  fpprbasnn  44715  fpprnn  44716  sbgoldbaltlem1  44765  nnsum3primesle9  44780  bgoldbtbndlem1  44791  bgoldbtbndlem2  44792  isomuspgrlem2d  44817  upwlkbprop  44834  mgmpropd  44863  clcllaw  44919  intop  44931  assintop  44937  assintopcllaw  44940  rngimf1o  44997  rngimrnghm  44998  c0snmgmhm  45006  elrngchom  45060  rnghmsubcsetclem1  45067  rnghmsubcsetclem2  45068  rngcid  45071  rngcinv  45073  rngciso  45074  elrngchomALTV  45078  rngccatidALTV  45081  rngcinvALTV  45085  rngcisoALTV  45086  funcrngcsetcALT  45091  zrinitorngc  45092  zrtermorngc  45093  elringchom  45106  rhmsubcsetclem1  45113  rhmsubcsetclem2  45114  ringcid  45117  rhmsubcrngclem1  45119  rhmsubcrngclem2  45120  ringcinv  45124  ringciso  45125  funcringcsetcALTV2lem7  45134  elringchomALTV  45141  ringccatidALTV  45144  ringcinvALTV  45148  ringcisoALTV  45149  funcringcsetclem7ALTV  45157  irinitoringc  45161  zrtermoringc  45162  rhmsubclem3  45180  rhmsubclem4  45181  rhmsubcALTVlem3  45198  rhmsubcALTVlem4  45199  ztprmneprm  45217  suppmptcfin  45249  linccl  45289  linc1  45300  lincolss  45309  ldepspr  45348  nn0sumshdiglem1  45501  0aryfvalelfv  45515  rrxlines  45613  rrxsphere  45628  itsclc0yqsol  45644  itschlc0xyqsol1  45646  fvconstr2  45708