Theorem syl6ibr 241

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 10-Jan-1993.)

Hypotheses

Ref	Expression
syl6ibr.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl6ibr.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
syl6ibr	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6ibr.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	biimpri 217	. 2 ⊢ (𝜒 → 𝜃)
4	1, 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:  3imtr4g  284  imp4aOLD  613  nic-ax  1589  nfimdOLD  2214  mo2v  2465  euim  2511  mopick2  2528  2moswap  2535  2eu6  2546  necon3d  2803  necon1d  2804  ralrimd  2942  spcimegf  3260  spcegf  3262  spcimedv  3265  spc2gv  3269  spc3gv  3271  rspcimedv  3284  eqsbc3rOLD  3460  tpid3gOLD  4249  pwpw0  4284  sssn  4298  pwsnALT  4367  ssiun  4498  ssiun2  4499  wefrc  5032  ssrel  5130  dmcosseq  5308  relssres  5357  restidsingOLD  5378  trin2  5438  ssrnres  5491  sossfld  5499  wfisg  5632  tron  5663  ordtri3or  5672  oneqmini  5693  fnun  5911  f1oun  6069  brprcneu  6096  ssimaex  6173  chfnrn  6236  dffo4  6283  dffo5  6284  tpres  6371  fvclss  6404  isomin  6487  isofrlem  6490  isoselem  6491  fnoprabg  6659  nnsuc  6974  f1oweALT  7043  bropopvvv  7142  bropfvvvvlem  7143  frxp  7174  poxp  7176  fnse  7181  mpt2xopynvov0g  7227  issmo2  7333  smores  7336  smogt  7351  rdglim2  7415  tz7.48lem  7423  tz7.49  7427  swoer  7659  qsss  7695  domtriord  7991  pssnn  8063  ssfi  8065  findcard  8084  findcard2  8085  findcard3  8088  frfi  8090  dffi3  8220  supmo  8241  infmo  8284  inf3lem4  8411  carddom2  8686  fidomtri2  8703  pm54.43  8709  infpwfien  8768  alephordi  8780  cardaleph  8795  carduniima  8802  cardinfima  8803  alephval3  8816  dfac5lem4  8832  dfac5  8834  dfac2  8836  kmlem2  8856  cflm  8955  cfslb2n  8973  cfsmolem  8975  isf32lem9  9066  axcc4  9144  domtriomlem  9147  zorn2lem4  9204  zorn2lem6  9206  fpwwe2lem11  9341  fpwwe2lem12  9342  inttsk  9475  inar1  9476  intgru  9515  ingru  9516  indpi  9608  nqpr  9715  ltaddpr  9735  ltexprlem1  9737  ltexprlem5  9741  reclem2pr  9749  reclem4pr  9751  negn0  10338  zmulcl  11303  uzm1  11594  uzwo  11627  xmullem2  11967  icoshft  12165  difreicc  12175  fzouzsplit  12372  ssfzoulel  12428  seqf1olem1  12702  seqf1olem2  12703  hashge2el2difr  13118  hashtpg  13121  swrdccatin2  13338  modfsummod  14367  incexclem  14407  sqrt2irr  14817  dvds2lem  14832  dvdslelem  14869  oddnn02np1  14910  divalglem8  14961  dfgcd2  15101  euclemma  15263  iserodd  15378  ramcl  15571  mreiincl  16079  joinfval  16824  meetfval  16838  dirge  17060  sylow2alem1  17855  efgredlemb  17982  kerf1hrm  18566  lbspss  18903  lspsneu  18944  lspsnat  18966  lspsncv0  18967  opsrtoslem2  19306  distop  20610  epttop  20623  isclo2  20702  restdis  20792  subbascn  20868  cnrest2  20900  cnpresti  20902  isnrm2  20972  cmpsublem  21012  cmpcld  21015  dfcon2  21032  t1conperf  21049  1stcrest  21066  lly1stc  21109  uptx  21238  txcn  21239  prdstopn  21241  txcon  21302  cmphaushmeo  21413  fbasrn  21498  csdfil  21508  trufil  21524  fclscf  21639  alexsubALTlem3  21663  alexsubALT  21665  haustsms2  21750  ovoliunlem1  23077  ovoliunnul  23082  volsup2  23179  coeaddlem  23809  plymul0or  23840  radcnv0  23974  wilthlem3  24596  chtub  24737  gausslemma2dlem1a  24890  2sqlem10  24953  pntpbnd1  25075  mptelee  25575  axeuclidlem  25642  axcontlem4  25647  usgrarnedg  25913  usgraedg4  25916  frgrancvvdeqlemA  26564  frgrancvvdeqlemC  26566  isch3  27482  shmodsi  27632  orthin  27689  h1datomi  27824  stcltr2i  28518  atom1d  28596  sumdmdii  28658  cdj3lem1  28677  disjpreima  28779  lmxrge0  29326  dmvlsiga  29519  sibfof  29729  bnj600  30243  bnj1018  30286  bnj1173  30324  bnj1174  30325  erdszelem9  30435  cvmlift2lem1  30538  fundmpss  30910  tfisg  30960  frinsg  30986  poseq  30994  sltval2  31053  nodenselem7  31086  nofulllem5  31105  outsideofrflx  31404  nn0prpwlem  31487  ivthALT  31500  fnessref  31522  neibastop2lem  31525  tailfb  31542  bj-axtd  31751  bj-ssbequ1  31833  bj-nfdt0  31872  bj-nfimt  32025  bj-2upleq  32193  bj-restn0  32224  icorempt2  32375  isbasisrelowllem2  32380  matunitlindflem1  32575  poimirlem3  32582  poimirlem4  32583  poimirlem29  32608  mblfinlem3  32618  itg2addnclem3  32633  cover2  32678  fdc  32711  nninfnub  32717  equivtotbnd  32747  prdstotbnd  32763  cntotbnd  32765  ablo4pnp  32849  isdrngo3  32928  crngohomfo  32975  intidl  32998  or32dd  33066  prtlem18  33180  prter2  33184  lsat0cv  33338  lfl1  33375  lkreqN  33475  atlrelat1  33626  pmaple  34065  pmapsub  34072  pclclN  34195  pclfinN  34204  osumcllem4N  34263  pexmidlem1N  34274  cdleme7ga  34553  lcfl7N  35808  ss2iundf  36970  brtrclfv2  37038  nzss  37538  3impexpbicom  37706  alrim3con13v  37764  tratrb  37767  onfrALTlem3  37780  onfrALTlem2  37782  onfrALTlem1  37784  trsspwALT2  38068  trsspwALT3  38069  2reu1  39835  lighneallem4b  40064  bgoldbwt  40199  bgoldbst  40200  sgoldbalt  40203  lswn0  40242  uhgrissubgr  40499  nbgrnself2  40585  wlkOnl1iedg  40873  pthdivtx  40935  1wlkiswwlksupgr2  41074  eucrct2eupth  41413  2zrngamgm  41729  fldivexpfllog2  42157  ssdifsn  42228