Theorem syl6bi 242

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  ax12i  1866  sb3  2343  2eu2  2542  reu6  3362  sseq0  3927  disjel  3975  disjpss  3980  uneqdifeqOLD  4010  preq12b  4322  prel12  4323  prneimg  4328  elinti  4420  zfrepclf  4705  dtru  4783  opth1g  4873  propeqop  4895  otsndisj  4904  otiunsndisj  4905  iunopeqop  4906  elreldm  5271  issref  5428  relcnvtr  5572  relresfld  5579  ordtr2  5685  ordssun  5744  funopg  5836  funimass2  5886  f0dom0  6002  elfv2ex  6139  fveqdmss  6262  eldmrexrnb  6274  fvcofneq  6275  funopsn  6319  funsndifnop  6321  elunirn  6413  oprabid  6576  brfvopab  6598  limuni3  6944  peano5  6981  op1steq  7101  el2mpt2csbcl  7137  bropopvvv  7142  bropfvvvv  7144  f1o2ndf1  7172  frxp  7174  fnwelem  7179  suppimacnv  7193  fvn0elsuppb  7199  suppfnss  7207  reldmtpos  7247  rntpos  7252  seqomlem2  7433  oaordi  7513  oa00  7526  oalimcl  7527  omeulem1  7549  nnaordi  7585  ecopovtrn  7737  undifixp  7830  mapdom2  8016  unxpdomlem3  8051  enp1i  8080  findcard2  8085  infssuni  8140  wdompwdom  8366  opthreg  8398  inf3lemd  8407  inf3lem2  8409  inf3lem6  8413  cnfcomlem  8479  cnfcom3  8484  karden  8641  carden2a  8675  alephdom  8787  dfac5lem4  8832  dfac12r  8851  kmlem2  8856  kmlem12  8866  cfslb2n  8973  alephsing  8981  fin23lem30  9047  fin1a2lem6  9110  fin1a2lem13  9117  axcc2lem  9141  domtriomlem  9147  axdc3lem2  9156  axdc4lem  9160  brdom6disj  9235  alephexp1  9280  pwfseq  9365  addnidpi  9602  indpi  9608  nqereu  9630  ltsonq  9670  distrlem5pr  9728  addcanpr  9747  suplem1pr  9753  suplem2pr  9754  ltsrpr  9777  ltsosr  9794  sqgt0sr  9806  leltne  10006  ltnsym  10014  ltlen  10017  eqlei  10026  eqlei2  10027  infm3  10861  nnunb  11165  0mnnnnn0  11202  elnnnn0b  11214  nn0ge2m1nn  11237  btwnz  11355  uz11  11586  zq  11670  xrleltne  11854  xltnegi  11921  xnn0xadd0  11949  xmulasslem2  11984  reltxrnmnf  12043  icogelb  12096  iccleub  12100  uznfz  12292  2ffzeq  12329  elfzonlteqm1  12410  elfznelfzob  12440  injresinjlem  12450  injresinj  12451  fleqceilz  12515  modadd1  12569  modmul1  12585  modirr  12603  addmodlteq  12607  uzrdgfni  12619  fsuppmapnn0fiub0  12655  fsuppmapnn0ub  12657  seqf1o  12704  hashrabsn01  13023  hashrabsn1  13024  hash1snb  13068  hashf1lem2  13097  hash2prde  13109  hash2prd  13114  hash2pwpr  13115  hashge2el2dif  13117  hashge2el2difr  13118  fundmge2nop0  13129  ffz0iswrd  13187  ccatrcl1  13229  2swrd1eqwrdeq  13306  wrdind  13328  wrd2ind  13329  swrdccatin1  13334  swrdccat3blem  13346  2cshwcshw  13422  cshwcsh2id  13425  cshimadifsn  13426  2swrd2eqwrdeq  13544  wwlktovf  13547  wwlktovfo  13549  s3sndisj  13554  s3iunsndisj  13555  relexpindlem  13651  rexico  13941  lo1le  14230  fsum2dlem  14343  ntrivcvg  14468  fprodss  14517  fprod2dlem  14549  0dvds  14840  zeneo  14901  mod2eq1n2dvds  14909  opoe  14925  omoe  14926  opeo  14927  omeo  14928  m1exp1  14931  nn0o1gt2  14935  gcdneg  15081  dfgcd2  15101  algcvga  15130  eucalglt  15136  lcmf  15184  coprmdvds  15204  divgcdcoprmex  15218  cncongr1  15219  prm2orodd  15242  prm23lt5  15357  pockthi  15449  prmreclem5  15462  ramtcl2  15553  cshwrepswhash1  15647  f1ocpbl  16008  f1ovscpbl  16009  f1olecpbl  16010  monhom  16218  epihom  16225  inveq  16257  invcoisoid  16275  isocoinvid  16276  ciclcl  16285  cicrcl  16286  isinitoi  16476  istermoi  16477  2initoinv  16483  2termoinv  16490  setciso  16564  embedsetcestrclem  16620  ipopos  16983  gsumval2a  17102  ismnddef  17119  dfgrp2e  17271  symg2bas  17641  symgfix2  17659  gsmsymgreq  17675  pmtrdifellem4  17722  mndodcongi  17785  pj1eu  17932  dprd2da  18264  rimf1o  18557  rimrhm  18558  brric2  18568  lmodfopnelem1  18722  lspdisjb  18947  lspsnsubn0  18961  0ring01eq  19092  psrbaglefi  19193  obs2ss  19892  mamufacex  20014  mat0dim0  20092  mat0dimid  20093  mat0dimscm  20094  dmatmat  20119  scmatmat  20134  mat1scmat  20164  1mavmul  20173  mavmulsolcl  20176  gsummatr01  20284  cpmatpmat  20334  cpmadugsumlemF  20500  tg2  20580  tgcl  20584  neii1  20720  neii2  20722  neindisj2  20737  perfopn  20799  ordtbas2  20805  pnfnei  20834  mnfnei  20835  llyidm  21101  txlm  21261  qtopuni  21315  tgqtop  21325  isfild  21472  snfil  21478  fbunfip  21483  fgss2  21488  fmco  21575  fbflim2  21591  cnpflf2  21614  fcfelbas  21650  fcfneii  21651  alexsubALTlem2  21662  alexsubALT  21665  tgpconcompeqg  21725  tsmscl  21748  tngngpim  22273  tgioo  22407  xrsmopn  22423  iccntr  22432  reconnlem2  22438  addcnlem  22475  htpycn  22580  phtpyhtpy  22589  pi1blem  22647  fgcfil  22877  ioombl1lem4  23136  dyadmbl  23174  itg2gt0  23333  ditgneg  23427  dvivthlem1  23575  coeeq2  23802  aannenlem2  23888  sineq0  24077  efif1o  24096  leibpilem1  24467  xrlimcnp  24495  vmacl  24644  efvmacl  24646  vmalelog  24730  dchrelbasd  24764  lgsqr  24876  gausslemma2dlem0i  24889  2lgslem2  24920  2lgs  24932  2lgsoddprmlem3  24939  uhgr0vb  25738  umgrupgr  25769  umgrnloopv  25772  umgredgprv  25773  umgrislfupgrlem  25788  umgredg  25812  uhgra0v  25839  umisuhgra  25856  uslisushgra  25892  uslisumgra  25893  usisuslgra  25894  usgra0v  25900  usgraedgprv  25905  usgra2edg  25911  usgrarnedg  25913  usgraedg4  25916  usgra1v  25919  usgrafisindb0  25937  usgrafisindb1  25938  nbgra0nb  25958  nbcusgra  25992  cusgrasize2inds  26005  cusgrafilem2  26008  usgrasscusgra  26011  uvtxisvtx  26018  2mwlk  26049  wlkcpr  26057  edgwlk  26059  usgrwlknloop  26093  pthistrl  26102  spthonepeq  26117  wlkdvspthlem  26137  usgra2adedgspthlem2  26140  usgra2adedgwlkonALT  26144  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  usgra2wlkspth  26149  crctistrl  26156  cyclispth  26157  cyclispthon  26161  fargshiftf  26164  fargshiftfo  26166  usgrcyclnl2  26169  3v3e3cycl1  26172  constr3trllem2  26179  4cycl4v4e  26194  4cycl4dv  26195  4cycl4dv4e  26196  wwlknimp  26215  wwlkiswwlkn  26230  2wlkeq  26235  usg2wlkeq  26236  wwlkextproplem3  26271  wwlkextprop  26272  clwwlkprop  26298  clwwlkgt0  26299  clwwlknprop  26300  clwwlknimp  26304  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem1  26315  clwwlkisclwwlkn  26319  clwwlkext2edg  26330  hashecclwwlkn1  26361  usghashecclwwlk  26362  clwlkf1clwwlklem  26376  el2wlkonotlem  26389  el2wlkonot  26396  el2wlkonotot0  26399  2wlkonot3v  26402  2spthonot3v  26403  el2wlksotot  26409  usg2wlkonot  26410  2spontn0vne  26414  vdgr1a  26433  hashnbgravdg  26440  0eusgraiff0rgracl  26468  rusgrasn  26472  rusgra0edg  26482  clwlknclwlkdifs  26487  frgra3vlem2  26528  1to2vfriswmgra  26533  1to3vfriswmgra  26534  vdfrgra0  26549  vdn0frgrav2  26550  vdgn0frgrav2  26551  frgrancvvdeqlem2  26558  frgrancvvdeqlem4  26560  frgrancvvdeqlemC  26566  usgreghash2spotv  26593  frgregordn0  26597  numclwwlkovf2ex  26613  numclwlk1lem2f1  26621  frgrareggt1  26643  frgrareg  26644  frgraregord013  26645  frgraregord13  26646  nmlno0lem  27032  normgt0  27368  ocin  27539  nmlnop0iALT  28238  nmopun  28257  cvpss  28528  cvnbtwn  28529  atcvati  28629  mdsymlem6  28651  issgon  29513  mbfmcnt  29657  ballotlemfc0  29881  ballotlemfcc  29882  mthmblem  30731  dfres3  30902  sltsgn1  31058  sltsgn2  31059  sltintdifex  31060  sltres  31061  pprodss4v  31161  funpartfun  31220  funpartfv  31222  5segofs  31283  btwnxfr  31333  brofs2  31354  brifs2  31355  btwnconn1  31378  segleantisym  31392  broutsideof2  31399  outsidene1  31400  outsidene2  31401  funray  31417  lineunray  31424  cldbnd  31491  bj-ax12iOLD  31804  bj-dtru  31985  topdifinffinlem  32371  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlpssretop  32388  matunitlindf  32577  poimir  32612  volsupnfl  32624  itg2addnclem  32631  cover2  32678  sdclem2  32708  fdc  32711  sstotbnd3  32745  heibor1  32779  clmgmOLD  32820  smgrpmgm  32833  smgrpassOLD  32834  dvrunz  32923  0rngo  32996  lsatcvat  33355  lshpkrex  33423  cmtbr3N  33559  atn0  33613  atnle  33622  cvlsupr4  33650  cvlsupr5  33651  cvlsupr6  33652  cvrval4N  33718  cvratlem  33725  2llnjN  33871  2lplnj  33924  linepsubN  34056  elpaddatiN  34109  elpcliN  34197  pclcmpatN  34205  ldilval  34417  ltrnu  34425  cdleme18d  34600  tendotp  35067  tendof  35069  tendovalco  35071  diatrl  35351  diaintclN  35365  dvheveccl  35419  dibintclN  35474  dihord6apre  35563  dihmeetlem1N  35597  dihpN  35643  dihintcl  35651  dochkrshp4  35696  pw2f1ocnv  36622  iocinico  36816  expgrowthi  37554  iotavalsb  37656  bi23imp1  37722  ioogtlb  38564  iocgtlb  38571  iocleub  38572  icoltub  38579  iooltub  38582  stoweidlem31  38924  2reu2  39836  eu2ndop1stv  39851  funressnfv  39857  afvelrnb0  39893  el1fzopredsuc  39948  iccpartimp  39955  iccpartrn  39968  iccpartf  39969  iccpartnel  39976  fmtnofac1  40020  prmdvdsfmtnof1lem2  40035  31prm  40050  lighneallem3  40062  nn0o1gt2ALTV  40143  nn0oALTV  40145  sgoldbaltlem1  40201  nnsum3primesle9  40210  bgoldbtbndlem1  40221  bgoldbtbndlem2  40222  pfxsuff1eqwrdeq  40270  otiunsndisjX  40317  2f1fvneq  40322  fzoopth  40360  2ffzoeq  40361  elfzr  40364  elfzo0l  40365  elfzlmr  40366  hash1n0  40370  uspgrushgr  40405  uspgrupgr  40406  usgruspgr  40408  usgredgprvALT  40422  usgrnloopvALT  40428  uhgr2edg  40435  edg0usgr  40479  egrsubgr  40501  0uhgrsubgr  40503  uhgrspansubgrlem  40514  nbuhgr  40565  nbgrisvtx  40581  uvtxaisvtx  40615  vtxnbuvtx  40617  uvtx2vtx1edg  40625  cusgrsize2inds  40669  cusgrfilem2  40672  vtxdg0v  40688  1loopgrnb0  40717  wlkbProp  40817  2m1wlk  40818  1wlkvtxeledg  40828  1wlkeq  40838  1wlkl1loop  40842  1wlk1walk  40843  upgrwlkedg  40850  uspgr2wlkeq  40854  1wlkv0  40859  wlkOnl1iedg  40873  wlkOn2n0  40874  1wlkp1lem8  40889  1wlkp1  40890  lfgrwlkprop  40896  lfgr1wlknloop  40898  trlis1wlk  40905  trlf1  40906  PthisTrl  40931  pthdivtx  40935  spthdep  40940  pthdepissPth  40941  spthonepeq-av  40958  uhgr1wlkspthlem2  40960  usgr2wlkneq  40962  usgr2trlncl  40966  usgr2trlspth  40967  pthdlem2lem  40973  clwlkis1wlk  40981  cyclisPthon  41007  uspgrn2crct  41011  wwlks  41038  wwlknbp  41044  0enwwlksnge1  41060  wwlkswwlksn  41061  1wlklnwwlkln1  41065  wwlksnextproplem3  41117  wwlksnextprop  41118  wspthsnonn0vne  41124  2pthon3v-av  41150  umgr2adedgspth  41155  wwlks2onv  41158  rusgr0edg  41176  clwwlknclwwlkdifs  41181  clwwlknbp0  41192  isclwwlksnx  41197  clwwlkclwwlkn  41199  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a4  41206  clwlkclwwlklem2  41209  clwwlksext2edg  41230  erclwwlksneqlen  41252  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfclwwlk  41269  clwlksf1clwwlklem  41275  upgr11wlkdlem1  41312  upgr3v3e3cycl  41347  uhgr3cyclexlem  41348  1conngr  41361  conngrv2edg  41362  eupth2lem3lem4  41399  eulercrct  41410  frgrusgrfrcond  41431  frgr3vlem2  41444  1to2vfriswmgr  41449  1to3vfriswmgr  41450  frgrncvvdeqlem2  41470  frgrncvvdeqlem4  41472  frgrncvvdeqlemC  41478  fusgreghash2wspv  41499  fusgreg2wsp  41500  frrusgrord0  41503  av-numclwwlkovf2ex  41517  av-numclwlk1lem2f1  41524  av-frgrareggt1  41547  av-frgraregord013  41549  av-frgraregord13  41550  mgmpropd  41565  clcllaw  41617  intop  41629  assintop  41635  assintopcllaw  41638  rngimf1o  41695  rngimrnghm  41696  c0snmgmhm  41704  elrngchom  41760  rnghmsubcsetclem1  41767  rnghmsubcsetclem2  41768  rngcid  41771  rngcinv  41773  rngciso  41774  elrngchomALTV  41778  rngccatidALTV  41781  rngcinvALTV  41785  rngcisoALTV  41786  funcrngcsetcALT  41791  zrinitorngc  41792  zrtermorngc  41793  elringchom  41806  rhmsubcsetclem1  41813  rhmsubcsetclem2  41814  ringcid  41817  rhmsubcrngclem1  41819  rhmsubcrngclem2  41820  ringcinv  41824  ringciso  41825  funcringcsetcALTV2lem7  41834  elringchomALTV  41841  ringccatidALTV  41844  ringcinvALTV  41848  ringcisoALTV  41849  funcringcsetclem7ALTV  41857  irinitoringc  41861  zrtermoringc  41862  rhmsubclem3  41880  rhmsubclem4  41881  rhmsubcALTVlem3  41899  rhmsubcALTVlem4  41900  ztprmneprm  41918  nn0le2is012  41938  suppmptcfin  41954  linccl  41997  linc1  42008  lincolss  42017  ldepspr  42056  nn0sumshdiglem1  42213