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  3722  2reu2  3892  sseq0  4399  disjel  4456  disjpss  4460  preq12b  4851  prneimg  4855  preqsnd  4859  elinti  4959  zfrepclf  5294  dtruALT2  5368  dtruOLD  5441  opth1g  5478  sbcop1  5488  snopeqop  5506  propeqop  5507  otsndisj  5519  otiunsndisj  5520  iunopeqop  5521  po2ne  5604  soasym  5619  elreldm  5933  dfres3  5985  relcnvtrg  6263  relresfld  6273  elpredimg  6313  ordtr2  6406  ordssun  6464  funopg  6580  funimass2  6629  f0dom0  6773  elfv2ex  6935  fveqdmss  7078  eldmrexrnb  7091  fvcofneq  7092  funopsn  7143  funopdmsn  7145  funsndifnop  7146  elunirn  7247  2f1fvneq  7256  oprabidw  7437  oprabid  7438  brfvopab  7463  limuni3  7838  peano5  7881  peano5OLD  7882  op1steq  8016  el2mpocsbcl  8068  bropopvvv  8073  bropfvvvv  8075  f1o2ndf1  8105  frxp  8109  fnwelem  8114  poxp2  8126  suppimacnv  8156  fvn0elsuppb  8163  suppfnss  8171  reldmtpos  8216  rntpos  8221  seqomlem2  8448  oaordi  8543  oa00  8556  oalimcl  8557  omeulem1  8579  nnaordi  8615  ecopovtrn  8811  undifixp  8925  mapdom2  9145  unxpdomlem3  9249  en1eqsn  9271  enp1iOLD  9277  findcard2OLD  9281  infssuni  9340  wdompwdom  9570  preleqg  9607  opthreg  9610  inf3lemd  9619  inf3lem2  9621  inf3lem6  9625  cnfcomlem  9691  cnfcom3  9696  karden  9887  carden2a  9958  alephdom  10073  dfac5lem4  10118  dfac12r  10138  kmlem2  10143  kmlem12  10153  cfslb2n  10260  alephsing  10268  fin23lem30  10334  fin1a2lem6  10397  fin1a2lem13  10404  axcc2lem  10428  domtriomlem  10434  axdc3lem2  10443  axdc4lem  10447  brdom6disj  10524  alephexp1  10571  pwfseq  10656  addnidpi  10893  indpi  10899  nqereu  10921  ltsonq  10961  distrlem5pr  11019  addcanpr  11038  suplem1pr  11044  suplem2pr  11045  ltsrpr  11069  ltsosr  11086  sqgt0sr  11098  leltne  11300  ltnsym  11309  ltlen  11312  eqlei  11321  eqlei2  11322  infm3  12170  nnunb  12465  0mnnnnn0  12501  elnnnn0b  12513  nn0ge2m1nn  12538  nn0le2is012  12623  btwnz  12662  uz11  12844  xrleltne  13121  xltnegi  13192  xnn0lenn0nn0  13221  xnn0xadd0  13223  xmulasslem2  13258  reltxrnmnf  13318  icogelb  13372  iccleub  13376  uznfz  13581  2ffzeq  13619  elfzonlteqm1  13705  elfzo0l  13719  elfznelfzob  13735  elfzr  13742  elfzlmr  13743  injresinjlem  13749  injresinj  13750  fleqceilz  13816  modadd1  13870  modmul1  13886  modirr  13904  addmodlteq  13908  uzrdgfni  13920  fsuppmapnn0fiub0  13955  fsuppmapnn0ub  13957  seqf1o  14006  expnngt1  14201  hashrabsn01  14330  hashrabsn1  14331  hash1snb  14376  hash1n0  14378  hashf1lem2  14414  hash2prde  14428  hash2prd  14433  hash2pwpr  14434  hashle2pr  14435  hashle2prv  14436  hashge2el2dif  14438  hashge2el2difr  14439  fundmge2nop0  14450  ffz0iswrd  14488  ccatrcl1  14541  pfxsuff1eqwrdeq  14646  wrdind  14669  wrd2ind  14670  swrdccatin1  14672  swrdccat3blem  14686  2cshwcshw  14773  cshwcsh2id  14776  cshimadifsn  14777  2swrd2eqwrdeq  14901  wwlktovf  14904  wwlktovfo  14906  s3sndisj  14911  s3iunsndisj  14912  relexpindlem  15007  rexico  15297  lo1le  15595  fsum2dlem  15713  ntrivcvg  15840  fprodss  15889  fprod2dlem  15921  0dvds  16217  mod2eq1n2dvds  16287  opoe  16303  omoe  16304  opeo  16305  omeo  16306  m1exp1  16316  nn0enne  16317  nn0o1gt2  16321  gcdneg  16460  dfgcd2  16485  algcvga  16513  eucalglt  16519  lcmf  16567  coprmdvds  16587  divgcdcoprmex  16600  cncongr1  16601  prm2orodd  16625  prm23lt5  16744  pockthi  16837  prmreclem5  16850  ramtcl2  16941  cshwrepswhash1  17033  f1ocpbl  17468  f1ovscpbl  17469  f1olecpbl  17470  monhom  17679  epihom  17686  inveq  17718  invcoisoid  17736  isocoinvid  17737  ciclcl  17746  cicrcl  17747  isinitoi  17946  istermoi  17947  2initoinv  17957  2termoinv  17964  setciso  18038  embedsetcestrclem  18106  ipopos  18486  gsumval2a  18601  ismnddef  18624  dfgrp2e  18845  symg2bas  19255  snsymgefmndeq  19257  symgvalstruct  19259  symgvalstructOLD  19260  symgfix2  19279  gsmsymgreq  19295  pmtrdifellem4  19342  mndodcongi  19406  pj1eu  19559  cycsubmcmn  19752  dprd2da  19907  0ring01eq  20297  lmodfopnelem1  20501  lspdisjb  20732  lspsnsubn0  20746  obs2ss  21276  psrbaglefiOLD  21478  mamufacex  21883  mat0dim0  21961  mat0dimid  21962  mat0dimscm  21963  dmatmat  21988  scmatmat  22003  mat1scmat  22033  1mavmul  22042  mavmulsolcl  22045  gsummatr01  22153  cpmatpmat  22204  cpmadugsumlemF  22370  tg2  22460  tgcl  22464  neii1  22602  neii2  22604  neindisj2  22619  perfopn  22681  ordtbas2  22687  pnfnei  22716  mnfnei  22717  llyidm  22984  txlm  23144  qtopuni  23198  tgqtop  23208  isfild  23354  snfil  23360  fbunfip  23365  fgss2  23370  fmco  23457  fbflim2  23473  cnpflf2  23496  fcfelbas  23532  fcfneii  23533  alexsubALTlem2  23544  alexsubALT  23547  tgpconncompeqg  23608  tsmscl  23631  tngngpim  24168  tgioo  24304  xrsmopn  24320  iccntr  24329  reconnlem2  24335  addcnlem  24372  htpycn  24481  phtpyhtpy  24490  pi1blem  24547  fgcfil  24780  ioombl1lem4  25070  dyadmbl  25109  itg2gt0  25270  ditgneg  25366  dvivthlem1  25517  coeeq2  25748  aannenlem2  25834  sineq0  26025  efif1o  26047  xrlimcnp  26463  vmacl  26612  efvmacl  26614  vmalelog  26698  dchrelbasd  26732  lgsqr  26844  lgsqrmodndvds  26846  gausslemma2dlem0i  26857  2lgslem2  26888  2lgs  26900  2lgsoddprmlem3  26907  2sqnn  26932  2sqreultlem  26940  2sqreultblem  26941  2sqreunnltlem  26943  2sqreunnltblem  26944  sltintdifex  27154  sltres  27155  nosepnelem  27172  nolt02o  27188  negsprop  27499  mulsprop  27576  elntg2  28233  uhgr0vb  28322  umgrupgr  28353  umgrnloopv  28356  umgredgprv  28357  umgrislfupgrlem  28372  umgredg  28388  uspgrushgr  28425  uspgrupgr  28426  usgruspgr  28428  usgredgprvALT  28442  usgrnloopvALT  28448  uhgr2edg  28455  edg0usgr  28500  egrsubgr  28524  0uhgrsubgr  28526  uhgrspansubgrlem  28537  nbuhgr  28590  cusgrsize2inds  28700  cusgrfilem2  28703  vtxdg0v  28720  1loopgrnb0  28749  vtxdginducedm1lem4  28789  wlkvtxeledg  28871  wlkeq  28881  wlkl1loop  28885  wlk1walk  28886  upgrwlkedg  28889  uspgr2wlkeq  28893  wlkv0  28898  wlkonl1iedg  28912  wlkon2n0  28913  wlkp1lem8  28927  wlkp1  28928  lfgrwlkprop  28934  lfgrwlknloop  28936  2pthnloop  28978  upgrwlkdvde  28984  spthonepeq  28999  uhgrwkspthlem2  29001  usgr2wlkneq  29003  usgr2trlncl  29007  usgr2trlspth  29008  pthdlem2lem  29014  clwlkcompbp  29029  uspgrn2crct  29052  wwlks  29079  wwlknbp  29086  0enwwlksnge1  29108  wwlkswwlksn  29109  wlklnwwlkln1  29112  wwlksnextproplem3  29155  wwlksnextprop  29156  wspthsnonn0vne  29161  wspn0  29168  2pthon3v  29187  umgr2adedgspth  29192  rusgr0edg  29217  clwwlkccat  29233  clwlkclwwlklem2fv2  29239  clwlkclwwlklem2a4  29240  clwlkclwwlklem2  29243  clwlkclwwlkflem  29247  clwwlknp  29280  clwwlkwwlksb  29297  clwwlkext2edg  29299  erclwwlkneqlen  29311  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  clwwlknonwwlknonb  29349  upgr1wlkdlem1  29388  upgr3v3e3cycl  29423  uhgr3cyclexlem  29424  1conngr  29437  conngrv2edg  29438  eupth2lem3lem4  29474  eulercrct  29485  isfrgr  29503  frgr3vlem2  29517  1to2vfriswmgr  29522  1to3vfriswmgr  29523  frgrncvvdeqlem9  29550  frgrwopreg  29566  frgr2wwlkeqm  29574  2wspmdisj  29580  numclwwlk1lem2f  29598  frgrreggt1  29636  frgrregord013  29638  frgrregord13  29639  l2p  29720  nmlno0lem  30034  normgt0  30368  ocin  30537  nmlnop0iALT  31236  nmopun  31255  cvpss  31526  cvnbtwn  31527  atcvati  31627  mdsymlem6  31649  iunrnmptss  31785  wrdt2ind  32105  irngssv  32741  issgon  33110  mbfmcnt  33256  ballotlemfc0  33480  ballotlemfcc  33481  satfv0  34338  satfv0fun  34351  fmla1  34367  gonarlem  34374  gonar  34375  goalrlem  34376  goalr  34377  fmla0disjsuc  34378  satffunlem  34381  satffunlem1lem1  34382  satffunlem2lem1  34384  satfun  34391  satfv0fvfmla0  34393  sategoelfv  34400  mthmblem  34560  pprodss4v  34845  funpartfun  34904  funpartfv  34906  5segofs  34967  btwnxfr  35017  brofs2  35038  brifs2  35039  btwnconn1  35062  segleantisym  35076  broutsideof2  35083  outsidene1  35084  outsidene2  35085  funray  35101  lineunray  35108  cldbnd  35200  bj-imdirval3  36054  topdifinffinlem  36217  isbasisrelowllem1  36225  isbasisrelowllem2  36226  relowlpssretop  36234  inunissunidif  36245  pibt2  36287  matunitlindf  36475  poimir  36510  volsupnfl  36522  itg2addnclem  36528  cover2  36572  sdclem2  36599  fdc  36602  sstotbnd3  36633  heibor1  36667  clmgmOLD  36708  smgrpmgm  36721  smgrpassOLD  36722  dvrunz  36811  0rngo  36884  mopickr  37221  lsatcvat  37909  lshpkrex  37977  cmtbr3N  38113  atn0  38167  atnle  38176  cvlsupr4  38204  cvlsupr5  38205  cvlsupr6  38206  cvrval4N  38274  cvratlem  38281  2llnjN  38427  2lplnj  38480  linepsubN  38612  elpaddatiN  38665  elpcliN  38753  pclcmpatN  38761  ldilval  38973  ltrnu  38981  cdleme18d  39155  tendotp  39621  tendof  39623  tendovalco  39625  diatrl  39904  diaintclN  39918  dvheveccl  39972  dibintclN  40027  dihord6apre  40116  dihmeetlem1N  40150  dihpN  40196  dihintcl  40204  dochkrshp4  40249  oexpreposd  41208  pw2f1ocnv  41762  iocinico  41947  onsucf1olem  42006  succlg  42064  oacl2g  42066  omabs2  42068  omcl2  42069  naddcnfcom  42102  naddcnfass  42105  safesnsupfidom1o  42154  infordmin  42269  pr2cv  42285  expgrowthi  43078  iotavalsb  43178  bi23imp1  43242  ioogtlb  44195  iocgtlb  44202  iocleub  44203  icoltub  44208  iooltub  44210  stoweidlem31  44734  oppr  45727  funressnfv  45740  fsetsniunop  45746  fsetsnf1  45749  eu2ndop1stv  45820  afvelrnb0  45859  otiunsndisjX  45974  el1fzopredsuc  46020  fzoopth  46022  2ffzoeq  46023  uniimaprimaeqfv  46037  elsetpreimafveqfv  46047  iccpartimp  46072  iccpartrn  46085  iccpartf  46086  iccpartnel  46093  fargshiftf  46095  fargshiftfo  46097  ichnfimlem  46118  ichnfim  46119  ichreuopeq  46128  sprel  46139  sprsymrelfvlem  46145  sprsymrelfolem2  46148  prproropf1olem4  46161  prprelb  46171  poprelb  46179  fmtnofac1  46225  prmdvdsfmtnof1lem2  46240  31prm  46252  lighneallem3  46262  nn0o1gt2ALTV  46349  nn0oALTV  46351  odd2prm2  46373  mogoldbblem  46375  fpprbasnn  46384  fpprnn  46385  sbgoldbaltlem1  46434  nnsum3primesle9  46449  bgoldbtbndlem1  46460  bgoldbtbndlem2  46461  isomuspgrlem2d  46486  upwlkbprop  46503  mgmpropd  46532  clcllaw  46588  intop  46600  assintop  46606  assintopcllaw  46609  rngimf1o  46689  rngimrnghm  46690  c0snmgmhm  46699  elrngchom  46820  rnghmsubcsetclem1  46827  rnghmsubcsetclem2  46828  rngcid  46831  rngcinv  46833  rngciso  46834  elrngchomALTV  46838  rngccatidALTV  46841  rngcinvALTV  46845  rngcisoALTV  46846  funcrngcsetcALT  46851  zrinitorngc  46852  zrtermorngc  46853  elringchom  46866  rhmsubcsetclem1  46873  rhmsubcsetclem2  46874  ringcid  46877  rhmsubcrngclem1  46879  rhmsubcrngclem2  46880  ringciso  46885  funcringcsetcALTV2lem7  46894  elringchomALTV  46901  ringccatidALTV  46904  ringcisoALTV  46909  funcringcsetclem7ALTV  46917  irinitoringc  46921  zrtermoringc  46922  rhmsubclem3  46940  rhmsubclem4  46941  rhmsubcALTVlem3  46958  rhmsubcALTVlem4  46959  ztprmneprm  46977  suppmptcfin  47009  linccl  47049  linc1  47060  lincolss  47069  ldepspr  47108  nn0sumshdiglem1  47261  0aryfvalelfv  47275  rrxlines  47373  rrxsphere  47388  itsclc0yqsol  47404  itschlc0xyqsol1  47406  fdomne0  47470  f002  47474  fvconstr2  47478  fullthinc  47620