Theorem syl6bi 252

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  sb3OLD  2481  sb1OLD  2482  sb4a  2484  hbsb2  2486  dfsb2  2497  2eu2  2654  nfabdwOLD  2930  reu6  3656  2reu2  3827  sseq0  4330  disjel  4387  disjpss  4391  preq12b  4778  prneimg  4782  preqsnd  4786  elinti  4885  zfrepclf  5213  dtru  5288  opth1g  5387  sbcop1  5396  snopeqop  5414  propeqop  5415  otsndisj  5427  otiunsndisj  5428  iunopeqop  5429  po2ne  5510  soasym  5525  elreldm  5833  dfres3  5885  relcnvtrg  6159  relresfld  6168  elpredimg  6206  ordtr2  6295  ordssun  6350  funopg  6452  funimass2  6501  f0dom0  6642  elfv2ex  6797  fveqdmss  6938  eldmrexrnb  6950  fvcofneq  6951  funopsn  7002  funopdmsn  7004  funsndifnop  7005  elunirn  7106  2f1fvneq  7114  oprabidw  7286  oprabid  7287  brfvopab  7310  limuni3  7674  peano5  7714  peano5OLD  7715  op1steq  7848  el2mpocsbcl  7896  bropopvvv  7901  bropfvvvv  7903  f1o2ndf1  7934  frxp  7938  fnwelem  7943  suppimacnv  7961  fvn0elsuppb  7968  suppfnss  7976  reldmtpos  8021  rntpos  8026  seqomlem2  8252  oaordi  8339  oa00  8352  oalimcl  8353  omeulem1  8375  nnaordi  8411  ecopovtrn  8567  undifixp  8680  mapdom2  8884  unxpdomlem3  8958  enp1i  8982  findcard2OLD  8986  infssuni  9040  wdompwdom  9267  preleqg  9303  opthreg  9306  inf3lemd  9315  inf3lem2  9317  inf3lem6  9321  cnfcomlem  9387  cnfcom3  9392  karden  9584  carden2a  9655  alephdom  9768  dfac5lem4  9813  dfac12r  9833  kmlem2  9838  kmlem12  9848  cfslb2n  9955  alephsing  9963  fin23lem30  10029  fin1a2lem6  10092  fin1a2lem13  10099  axcc2lem  10123  domtriomlem  10129  axdc3lem2  10138  axdc4lem  10142  brdom6disj  10219  alephexp1  10266  pwfseq  10351  addnidpi  10588  indpi  10594  nqereu  10616  ltsonq  10656  distrlem5pr  10714  addcanpr  10733  suplem1pr  10739  suplem2pr  10740  ltsrpr  10764  ltsosr  10781  sqgt0sr  10793  leltne  10995  ltnsym  11003  ltlen  11006  eqlei  11015  eqlei2  11016  infm3  11864  nnunb  12159  0mnnnnn0  12195  elnnnn0b  12207  nn0ge2m1nn  12232  nn0le2is012  12314  btwnz  12352  uz11  12536  xrleltne  12808  xltnegi  12879  xnn0lenn0nn0  12908  xnn0xadd0  12910  xmulasslem2  12945  reltxrnmnf  13005  icogelb  13059  iccleub  13063  uznfz  13268  2ffzeq  13306  elfzonlteqm1  13391  elfzo0l  13405  elfznelfzob  13421  elfzr  13428  elfzlmr  13429  injresinjlem  13435  injresinj  13436  fleqceilz  13502  modadd1  13556  modmul1  13572  modirr  13590  addmodlteq  13594  uzrdgfni  13606  fsuppmapnn0fiub0  13641  fsuppmapnn0ub  13643  seqf1o  13692  expnngt1  13884  hashrabsn01  14016  hashrabsn1  14017  hash1snb  14062  hash1n0  14064  hashf1lem2  14098  hash2prde  14112  hash2prd  14117  hash2pwpr  14118  hashle2pr  14119  hashle2prv  14120  hashge2el2dif  14122  hashge2el2difr  14123  fundmge2nop0  14134  ffz0iswrd  14172  ccatrcl1  14227  pfxsuff1eqwrdeq  14340  wrdind  14363  wrd2ind  14364  swrdccatin1  14366  swrdccat3blem  14380  2cshwcshw  14466  cshwcsh2id  14469  cshimadifsn  14470  2swrd2eqwrdeq  14594  wwlktovf  14599  wwlktovfo  14601  s3sndisj  14606  s3iunsndisj  14607  relexpindlem  14702  rexico  14993  lo1le  15291  fsum2dlem  15410  ntrivcvg  15537  fprodss  15586  fprod2dlem  15618  0dvds  15914  mod2eq1n2dvds  15984  opoe  16000  omoe  16001  opeo  16002  omeo  16003  m1exp1  16013  nn0enne  16014  nn0o1gt2  16018  gcdneg  16157  dfgcd2  16182  algcvga  16212  eucalglt  16218  lcmf  16266  coprmdvds  16286  divgcdcoprmex  16299  cncongr1  16300  prm2orodd  16324  prm23lt5  16443  pockthi  16536  prmreclem5  16549  ramtcl2  16640  cshwrepswhash1  16732  f1ocpbl  17153  f1ovscpbl  17154  f1olecpbl  17155  monhom  17364  epihom  17371  inveq  17403  invcoisoid  17421  isocoinvid  17422  ciclcl  17431  cicrcl  17432  isinitoi  17630  istermoi  17631  2initoinv  17641  2termoinv  17648  setciso  17722  embedsetcestrclem  17790  ipopos  18169  gsumval2a  18284  ismnddef  18302  dfgrp2e  18520  symg2bas  18915  snsymgefmndeq  18917  symgvalstruct  18919  symgvalstructOLD  18920  symgfix2  18939  gsmsymgreq  18955  pmtrdifellem4  19002  mndodcongi  19066  pj1eu  19217  cycsubmcmn  19404  dprd2da  19560  rimf1o  19893  rimrhm  19894  brric2  19904  lmodfopnelem1  20074  lspdisjb  20303  lspsnsubn0  20317  0ring01eq  20455  obs2ss  20846  psrbaglefiOLD  21046  mamufacex  21448  mat0dim0  21524  mat0dimid  21525  mat0dimscm  21526  dmatmat  21551  scmatmat  21566  mat1scmat  21596  1mavmul  21605  mavmulsolcl  21608  gsummatr01  21716  cpmatpmat  21767  cpmadugsumlemF  21933  tg2  22023  tgcl  22027  neii1  22165  neii2  22167  neindisj2  22182  perfopn  22244  ordtbas2  22250  pnfnei  22279  mnfnei  22280  llyidm  22547  txlm  22707  qtopuni  22761  tgqtop  22771  isfild  22917  snfil  22923  fbunfip  22928  fgss2  22933  fmco  23020  fbflim2  23036  cnpflf2  23059  fcfelbas  23095  fcfneii  23096  alexsubALTlem2  23107  alexsubALT  23110  tgpconncompeqg  23171  tsmscl  23194  tngngpim  23729  tgioo  23865  xrsmopn  23881  iccntr  23890  reconnlem2  23896  addcnlem  23933  htpycn  24042  phtpyhtpy  24051  pi1blem  24108  fgcfil  24340  ioombl1lem4  24630  dyadmbl  24669  itg2gt0  24830  ditgneg  24926  dvivthlem1  25077  coeeq2  25308  aannenlem2  25394  sineq0  25585  efif1o  25607  xrlimcnp  26023  vmacl  26172  efvmacl  26174  vmalelog  26258  dchrelbasd  26292  lgsqr  26404  lgsqrmodndvds  26406  gausslemma2dlem0i  26417  2lgslem2  26448  2lgs  26460  2lgsoddprmlem3  26467  2sqnn  26492  2sqreultlem  26500  2sqreultblem  26501  2sqreunnltlem  26503  2sqreunnltblem  26504  elntg2  27256  uhgr0vb  27345  umgrupgr  27376  umgrnloopv  27379  umgredgprv  27380  umgrislfupgrlem  27395  umgredg  27411  uspgrushgr  27448  uspgrupgr  27449  usgruspgr  27451  usgredgprvALT  27465  usgrnloopvALT  27471  uhgr2edg  27478  edg0usgr  27523  egrsubgr  27547  0uhgrsubgr  27549  uhgrspansubgrlem  27560  nbuhgr  27613  cusgrsize2inds  27723  cusgrfilem2  27726  vtxdg0v  27743  1loopgrnb0  27772  vtxdginducedm1lem4  27812  wlkvtxeledg  27893  wlkeq  27903  wlkl1loop  27907  wlk1walk  27908  upgrwlkedg  27911  uspgr2wlkeq  27915  wlkv0  27920  wlkonl1iedg  27935  wlkon2n0  27936  wlkp1lem8  27950  wlkp1  27951  lfgrwlkprop  27957  lfgrwlknloop  27959  2pthnloop  28000  upgrwlkdvde  28006  spthonepeq  28021  uhgrwkspthlem2  28023  usgr2wlkneq  28025  usgr2trlncl  28029  usgr2trlspth  28030  pthdlem2lem  28036  clwlkcompbp  28051  uspgrn2crct  28074  wwlks  28101  wwlknbp  28108  0enwwlksnge1  28130  wwlkswwlksn  28131  wlklnwwlkln1  28134  wwlksnextproplem3  28177  wwlksnextprop  28178  wspthsnonn0vne  28183  wspn0  28190  2pthon3v  28209  umgr2adedgspth  28214  rusgr0edg  28239  clwwlkccat  28255  clwlkclwwlklem2fv2  28261  clwlkclwwlklem2a4  28262  clwlkclwwlklem2  28265  clwlkclwwlkflem  28269  clwwlknp  28302  clwwlkwwlksb  28319  clwwlkext2edg  28321  erclwwlkneqlen  28333  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwwlknonwwlknonb  28371  upgr1wlkdlem1  28410  upgr3v3e3cycl  28445  uhgr3cyclexlem  28446  1conngr  28459  conngrv2edg  28460  eupth2lem3lem4  28496  eulercrct  28507  isfrgr  28525  frgr3vlem2  28539  1to2vfriswmgr  28544  1to3vfriswmgr  28545  frgrncvvdeqlem9  28572  frgrwopreg  28588  frgr2wwlkeqm  28596  2wspmdisj  28602  numclwwlk1lem2f  28620  frgrreggt1  28658  frgrregord013  28660  frgrregord13  28661  l2p  28742  nmlno0lem  29056  normgt0  29390  ocin  29559  nmlnop0iALT  30258  nmopun  30277  cvpss  30548  cvnbtwn  30549  atcvati  30649  mdsymlem6  30671  iunrnmptss  30806  wrdt2ind  31127  issgon  31991  mbfmcnt  32135  ballotlemfc0  32359  ballotlemfcc  32360  satfv0  33220  satfv0fun  33233  fmla1  33249  gonarlem  33256  gonar  33257  goalrlem  33258  goalr  33259  fmla0disjsuc  33260  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  satfun  33273  satfv0fvfmla0  33275  sategoelfv  33282  mthmblem  33442  poxp2  33717  sltintdifex  33791  sltres  33792  nosepnelem  33809  nolt02o  33825  pprodss4v  34113  funpartfun  34172  funpartfv  34174  5segofs  34235  btwnxfr  34285  brofs2  34306  brifs2  34307  btwnconn1  34330  segleantisym  34344  broutsideof2  34351  outsidene1  34352  outsidene2  34353  funray  34369  lineunray  34376  cldbnd  34442  bj-dtru  34926  bj-imdirval3  35282  topdifinffinlem  35445  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlpssretop  35462  inunissunidif  35473  pibt2  35515  matunitlindf  35702  poimir  35737  volsupnfl  35749  itg2addnclem  35755  cover2  35799  sdclem2  35827  fdc  35830  sstotbnd3  35861  heibor1  35895  clmgmOLD  35936  smgrpmgm  35949  smgrpassOLD  35950  dvrunz  36039  0rngo  36112  lsatcvat  36991  lshpkrex  37059  cmtbr3N  37195  atn0  37249  atnle  37258  cvlsupr4  37286  cvlsupr5  37287  cvlsupr6  37288  cvrval4N  37355  cvratlem  37362  2llnjN  37508  2lplnj  37561  linepsubN  37693  elpaddatiN  37746  elpcliN  37834  pclcmpatN  37842  ldilval  38054  ltrnu  38062  cdleme18d  38236  tendotp  38702  tendof  38704  tendovalco  38706  diatrl  38985  diaintclN  38999  dvheveccl  39053  dibintclN  39108  dihord6apre  39197  dihmeetlem1N  39231  dihpN  39277  dihintcl  39285  dochkrshp4  39330  oexpreposd  40242  pw2f1ocnv  40775  iocinico  40959  infordmin  41037  pr2cv  41044  expgrowthi  41840  iotavalsb  41940  bi23imp1  42004  ioogtlb  42923  iocgtlb  42930  iocleub  42931  icoltub  42936  iooltub  42938  stoweidlem31  43462  oppr  44411  funressnfv  44424  fsetsniunop  44430  fsetsnf1  44433  eu2ndop1stv  44504  afvelrnb0  44543  otiunsndisjX  44658  el1fzopredsuc  44705  fzoopth  44707  2ffzoeq  44708  uniimaprimaeqfv  44722  elsetpreimafveqfv  44732  iccpartimp  44757  iccpartrn  44770  iccpartf  44771  iccpartnel  44778  fargshiftf  44780  fargshiftfo  44782  ichnfimlem  44803  ichnfim  44804  ichreuopeq  44813  sprel  44824  sprsymrelfvlem  44830  sprsymrelfolem2  44833  prproropf1olem4  44846  prprelb  44856  poprelb  44864  fmtnofac1  44910  prmdvdsfmtnof1lem2  44925  31prm  44937  lighneallem3  44947  nn0o1gt2ALTV  45034  nn0oALTV  45036  odd2prm2  45058  mogoldbblem  45060  fpprbasnn  45069  fpprnn  45070  sbgoldbaltlem1  45119  nnsum3primesle9  45134  bgoldbtbndlem1  45145  bgoldbtbndlem2  45146  isomuspgrlem2d  45171  upwlkbprop  45188  mgmpropd  45217  clcllaw  45273  intop  45285  assintop  45291  assintopcllaw  45294  rngimf1o  45351  rngimrnghm  45352  c0snmgmhm  45360  elrngchom  45414  rnghmsubcsetclem1  45421  rnghmsubcsetclem2  45422  rngcid  45425  rngcinv  45427  rngciso  45428  elrngchomALTV  45432  rngccatidALTV  45435  rngcinvALTV  45439  rngcisoALTV  45440  funcrngcsetcALT  45445  zrinitorngc  45446  zrtermorngc  45447  elringchom  45460  rhmsubcsetclem1  45467  rhmsubcsetclem2  45468  ringcid  45471  rhmsubcrngclem1  45473  rhmsubcrngclem2  45474  ringcinv  45478  ringciso  45479  funcringcsetcALTV2lem7  45488  elringchomALTV  45495  ringccatidALTV  45498  ringcinvALTV  45502  ringcisoALTV  45503  funcringcsetclem7ALTV  45511  irinitoringc  45515  zrtermoringc  45516  rhmsubclem3  45534  rhmsubclem4  45535  rhmsubcALTVlem3  45552  rhmsubcALTVlem4  45553  ztprmneprm  45571  suppmptcfin  45603  linccl  45643  linc1  45654  lincolss  45663  ldepspr  45702  nn0sumshdiglem1  45855  0aryfvalelfv  45869  rrxlines  45967  rrxsphere  45982  itsclc0yqsol  45998  itschlc0xyqsol1  46000  fdomne0  46065  f002  46069  fvconstr2  46073  fullthinc  46215