Theorem syl6bi 255

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  ax12i  1969  sb3OLD  2505  sb1OLD  2507  sb4a  2509  hbsb2  2521  dfsb2  2532  2eu2  2737  nfabdw  3000  reu6  3717  2reu2  3882  sseq0  4353  disjel  4406  disjpss  4410  preq12b  4781  prneimg  4785  preqsnd  4789  elinti  4885  zfrepclf  5198  dtru  5271  opth1g  5370  sbcop1  5379  snopeqop  5396  propeqop  5397  otsndisj  5409  otiunsndisj  5410  iunopeqop  5411  po2ne  5489  soasym  5504  elreldm  5805  dfres3  5858  relcnvtrg  6119  relresfld  6127  ordtr2  6235  ordssun  6290  funopg  6389  funimass2  6437  f0dom0  6563  elfv2ex  6711  fveqdmss  6846  eldmrexrnb  6858  fvcofneq  6859  funopsn  6910  funopdmsn  6912  funsndifnop  6913  elunirn  7010  2f1fvneq  7018  oprabidw  7187  oprabid  7188  brfvopab  7211  limuni3  7567  peano5  7605  op1steq  7733  el2mpocsbcl  7780  bropopvvv  7785  bropfvvvv  7787  f1o2ndf1  7818  frxp  7820  fnwelem  7825  suppimacnv  7841  fvn0elsuppb  7847  suppfnss  7855  reldmtpos  7900  rntpos  7905  seqomlem2  8087  oaordi  8172  oa00  8185  oalimcl  8186  omeulem1  8208  nnaordi  8244  ecopovtrn  8400  undifixp  8498  mapdom2  8688  unxpdomlem3  8724  enp1i  8753  findcard2  8758  infssuni  8815  wdompwdom  9042  preleqg  9078  opthreg  9081  inf3lemd  9090  inf3lem2  9092  inf3lem6  9096  cnfcomlem  9162  cnfcom3  9167  karden  9324  carden2a  9395  alephdom  9507  dfac5lem4  9552  dfac12r  9572  kmlem2  9577  kmlem12  9587  cfslb2n  9690  alephsing  9698  fin23lem30  9764  fin1a2lem6  9827  fin1a2lem13  9834  axcc2lem  9858  domtriomlem  9864  axdc3lem2  9873  axdc4lem  9877  brdom6disj  9954  alephexp1  10001  pwfseq  10086  addnidpi  10323  indpi  10329  nqereu  10351  ltsonq  10391  distrlem5pr  10449  addcanpr  10468  suplem1pr  10474  suplem2pr  10475  ltsrpr  10499  ltsosr  10516  sqgt0sr  10528  leltne  10730  ltnsym  10738  ltlen  10741  eqlei  10750  eqlei2  10751  infm3  11600  nnunb  11894  0mnnnnn0  11930  elnnnn0b  11942  nn0ge2m1nn  11965  nn0le2is012  12047  btwnz  12085  uz11  12268  xrleltne  12539  xltnegi  12610  xnn0lenn0nn0  12639  xnn0xadd0  12641  xmulasslem2  12676  reltxrnmnf  12736  icogelb  12789  iccleub  12793  uznfz  12991  2ffzeq  13029  elfzonlteqm1  13114  elfzo0l  13128  elfznelfzob  13144  elfzr  13151  elfzlmr  13152  injresinjlem  13158  injresinj  13159  fleqceilz  13223  modadd1  13277  modmul1  13293  modirr  13311  addmodlteq  13315  uzrdgfni  13327  fsuppmapnn0fiub0  13362  fsuppmapnn0ub  13364  seqf1o  13412  expnngt1  13603  hashrabsn01  13735  hashrabsn1  13736  hash1snb  13781  hash1n0  13783  hashf1lem2  13815  hash2prde  13829  hash2prd  13834  hash2pwpr  13835  hashle2pr  13836  hashle2prv  13837  hashge2el2dif  13839  hashge2el2difr  13840  fundmge2nop0  13851  ffz0iswrd  13891  ffz0iswrdOLD  13892  ccatrcl1  13948  pfxsuff1eqwrdeq  14061  wrdind  14084  wrd2ind  14085  swrdccatin1  14087  swrdccat3blem  14101  2cshwcshw  14187  cshwcsh2id  14190  cshimadifsn  14191  2swrd2eqwrdeq  14315  wwlktovf  14320  wwlktovfo  14322  s3sndisj  14327  s3iunsndisj  14328  relexpindlem  14422  rexico  14713  lo1le  15008  fsum2dlem  15125  ntrivcvg  15253  fprodss  15302  fprod2dlem  15334  0dvds  15630  mod2eq1n2dvds  15696  opoe  15712  omoe  15713  opeo  15714  omeo  15715  m1exp1  15727  nn0enne  15728  nn0o1gt2  15732  gcdneg  15870  dfgcd2  15894  algcvga  15923  eucalglt  15929  lcmf  15977  coprmdvds  15997  divgcdcoprmex  16010  cncongr1  16011  prm2orodd  16035  prm23lt5  16151  pockthi  16243  prmreclem5  16256  ramtcl2  16347  cshwrepswhash1  16436  f1ocpbl  16798  f1ovscpbl  16799  f1olecpbl  16800  monhom  17005  epihom  17012  inveq  17044  invcoisoid  17062  isocoinvid  17063  ciclcl  17072  cicrcl  17073  isinitoi  17263  istermoi  17264  2initoinv  17270  2termoinv  17277  setciso  17351  embedsetcestrclem  17407  ipopos  17770  gsumval2a  17895  ismnddef  17913  dfgrp2e  18129  symg2bas  18521  snsymgefmndeq  18523  symgvalstruct  18525  symgfix2  18544  gsmsymgreq  18560  pmtrdifellem4  18607  mndodcongi  18671  pj1eu  18822  cycsubmcmn  19008  dprd2da  19164  rimf1o  19486  rimrhm  19487  brric2  19500  lmodfopnelem1  19670  lspdisjb  19898  lspsnsubn0  19912  0ring01eq  20044  psrbaglefi  20152  obs2ss  20873  mamufacex  21000  mat0dim0  21076  mat0dimid  21077  mat0dimscm  21078  dmatmat  21103  scmatmat  21118  mat1scmat  21148  1mavmul  21157  mavmulsolcl  21160  gsummatr01  21268  cpmatpmat  21318  cpmadugsumlemF  21484  tg2  21573  tgcl  21577  neii1  21714  neii2  21716  neindisj2  21731  perfopn  21793  ordtbas2  21799  pnfnei  21828  mnfnei  21829  llyidm  22096  txlm  22256  qtopuni  22310  tgqtop  22320  isfild  22466  snfil  22472  fbunfip  22477  fgss2  22482  fmco  22569  fbflim2  22585  cnpflf2  22608  fcfelbas  22644  fcfneii  22645  alexsubALTlem2  22656  alexsubALT  22659  tgpconncompeqg  22720  tsmscl  22743  tngngpim  23268  tgioo  23404  xrsmopn  23420  iccntr  23429  reconnlem2  23435  addcnlem  23472  htpycn  23577  phtpyhtpy  23586  pi1blem  23643  fgcfil  23874  ioombl1lem4  24162  dyadmbl  24201  itg2gt0  24361  ditgneg  24455  dvivthlem1  24605  coeeq2  24832  aannenlem2  24918  sineq0  25109  efif1o  25130  xrlimcnp  25546  vmacl  25695  efvmacl  25697  vmalelog  25781  dchrelbasd  25815  lgsqr  25927  lgsqrmodndvds  25929  gausslemma2dlem0i  25940  2lgslem2  25971  2lgs  25983  2lgsoddprmlem3  25990  2sqnn  26015  2sqreultlem  26023  2sqreultblem  26024  2sqreunnltlem  26026  2sqreunnltblem  26027  elntg2  26771  uhgr0vb  26857  umgrupgr  26888  umgrnloopv  26891  umgredgprv  26892  umgrislfupgrlem  26907  umgredg  26923  uspgrushgr  26960  uspgrupgr  26961  usgruspgr  26963  usgredgprvALT  26977  usgrnloopvALT  26983  uhgr2edg  26990  edg0usgr  27035  egrsubgr  27059  0uhgrsubgr  27061  uhgrspansubgrlem  27072  nbuhgr  27125  cusgrsize2inds  27235  cusgrfilem2  27238  vtxdg0v  27255  1loopgrnb0  27284  vtxdginducedm1lem4  27324  wlkvtxeledg  27405  wlkeq  27415  wlkl1loop  27419  wlk1walk  27420  upgrwlkedg  27423  uspgr2wlkeq  27427  wlkv0  27432  wlkonl1iedg  27447  wlkon2n0  27448  wlkp1lem8  27462  wlkp1  27463  lfgrwlkprop  27469  lfgrwlknloop  27471  2pthnloop  27512  upgrwlkdvde  27518  spthonepeq  27533  uhgrwkspthlem2  27535  usgr2wlkneq  27537  usgr2trlncl  27541  usgr2trlspth  27542  pthdlem2lem  27548  clwlkcompbp  27563  uspgrn2crct  27586  wwlks  27613  wwlknbp  27620  0enwwlksnge1  27642  wwlkswwlksn  27643  wlklnwwlkln1  27646  wwlksnextproplem3  27690  wwlksnextprop  27691  wspthsnonn0vne  27696  wspn0  27703  2pthon3v  27722  umgr2adedgspth  27727  rusgr0edg  27752  clwwlkccat  27768  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a4  27775  clwlkclwwlklem2  27778  clwlkclwwlkflem  27782  clwwlknp  27815  clwwlkwwlksb  27833  clwwlkext2edg  27835  erclwwlkneqlen  27847  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlknonwwlknonb  27885  upgr1wlkdlem1  27924  upgr3v3e3cycl  27959  uhgr3cyclexlem  27960  1conngr  27973  conngrv2edg  27974  eupth2lem3lem4  28010  eulercrct  28021  isfrgr  28039  frgr3vlem2  28053  1to2vfriswmgr  28058  1to3vfriswmgr  28059  frgrncvvdeqlem9  28086  frgrwopreg  28102  frgr2wwlkeqm  28110  2wspmdisj  28116  numclwwlk1lem2f  28134  frgrreggt1  28172  frgrregord013  28174  frgrregord13  28175  l2p  28256  nmlno0lem  28570  normgt0  28904  ocin  29073  nmlnop0iALT  29772  nmopun  29791  cvpss  30062  cvnbtwn  30063  atcvati  30163  mdsymlem6  30185  iunrnmptss  30317  wrdt2ind  30627  issgon  31382  mbfmcnt  31526  ballotlemfc0  31750  ballotlemfcc  31751  satfv0  32605  satfv0fun  32618  fmla1  32634  gonarlem  32641  gonar  32642  goalrlem  32643  goalr  32644  fmla0disjsuc  32645  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  satfun  32658  satfv0fvfmla0  32660  sategoelfv  32667  mthmblem  32827  sltintdifex  33168  sltres  33169  nosepnelem  33184  nolt02o  33199  pprodss4v  33345  funpartfun  33404  funpartfv  33406  5segofs  33467  btwnxfr  33517  brofs2  33538  brifs2  33539  btwnconn1  33562  segleantisym  33576  broutsideof2  33583  outsidene1  33584  outsidene2  33585  funray  33601  lineunray  33608  cldbnd  33674  bj-dtru  34139  bj-imdirval3  34477  topdifinffinlem  34631  isbasisrelowllem1  34639  isbasisrelowllem2  34640  relowlpssretop  34648  inunissunidif  34659  pibt2  34701  matunitlindf  34905  poimir  34940  volsupnfl  34952  itg2addnclem  34958  cover2  35004  sdclem2  35032  fdc  35035  sstotbnd3  35069  heibor1  35103  clmgmOLD  35144  smgrpmgm  35157  smgrpassOLD  35158  dvrunz  35247  0rngo  35320  lsatcvat  36201  lshpkrex  36269  cmtbr3N  36405  atn0  36459  atnle  36468  cvlsupr4  36496  cvlsupr5  36497  cvlsupr6  36498  cvrval4N  36565  cvratlem  36572  2llnjN  36718  2lplnj  36771  linepsubN  36903  elpaddatiN  36956  elpcliN  37044  pclcmpatN  37052  ldilval  37264  ltrnu  37272  cdleme18d  37446  tendotp  37912  tendof  37914  tendovalco  37916  diatrl  38195  diaintclN  38209  dvheveccl  38263  dibintclN  38318  dihord6apre  38407  dihmeetlem1N  38441  dihpN  38487  dihintcl  38495  dochkrshp4  38540  oexpreposd  39228  pw2f1ocnv  39683  iocinico  39867  infordmin  39948  pr2cv  39956  expgrowthi  40714  iotavalsb  40814  bi23imp1  40878  ioogtlb  41819  iocgtlb  41826  iocleub  41827  icoltub  41833  iooltub  41835  stoweidlem31  42365  oppr  43314  funressnfv  43327  eu2ndop1stv  43373  afvelrnb0  43412  otiunsndisjX  43527  el1fzopredsuc  43574  fzoopth  43576  2ffzoeq  43577  uniimaprimaeqfv  43591  elsetpreimafveqfv  43601  iccpartimp  43626  iccpartrn  43639  iccpartf  43640  iccpartnel  43647  fargshiftf  43649  fargshiftfo  43651  ichnfim  43673  ichreuopeq  43684  sprel  43695  sprsymrelfvlem  43701  sprsymrelfolem2  43704  prproropf1olem4  43717  prprelb  43727  poprelb  43735  fmtnofac1  43781  prmdvdsfmtnof1lem2  43796  31prm  43809  lighneallem3  43821  nn0o1gt2ALTV  43908  nn0oALTV  43910  odd2prm2  43932  mogoldbblem  43934  fpprbasnn  43943  fpprnn  43944  sbgoldbaltlem1  43993  nnsum3primesle9  44008  bgoldbtbndlem1  44019  bgoldbtbndlem2  44020  isomuspgrlem2d  44045  upwlkbprop  44062  mgmpropd  44091  clcllaw  44147  intop  44159  assintop  44165  assintopcllaw  44168  rngimf1o  44225  rngimrnghm  44226  c0snmgmhm  44234  elrngchom  44288  rnghmsubcsetclem1  44295  rnghmsubcsetclem2  44296  rngcid  44299  rngcinv  44301  rngciso  44302  elrngchomALTV  44306  rngccatidALTV  44309  rngcinvALTV  44313  rngcisoALTV  44314  funcrngcsetcALT  44319  zrinitorngc  44320  zrtermorngc  44321  elringchom  44334  rhmsubcsetclem1  44341  rhmsubcsetclem2  44342  ringcid  44345  rhmsubcrngclem1  44347  rhmsubcrngclem2  44348  ringcinv  44352  ringciso  44353  funcringcsetcALTV2lem7  44362  elringchomALTV  44369  ringccatidALTV  44372  ringcinvALTV  44376  ringcisoALTV  44377  funcringcsetclem7ALTV  44385  irinitoringc  44389  zrtermoringc  44390  rhmsubclem3  44408  rhmsubclem4  44409  rhmsubcALTVlem3  44426  rhmsubcALTVlem4  44427  ztprmneprm  44444  suppmptcfin  44476  linccl  44518  linc1  44529  lincolss  44538  ldepspr  44577  nn0sumshdiglem1  44730  rrxlines  44769  rrxsphere  44784  itsclc0yqsol  44800  itschlc0xyqsol1  44802