Theorem syl6ibr 251

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 227	. 2 ⊢ (𝜒 → 𝜃)
4	1, 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:  3imtr4g  295  nic-ax  1674  sbequ1  2239  dfmoeu  2534  2moswapv  2629  mopick2  2637  2moswap  2644  2eu6  2656  necon3d  2961  necon1d  2962  ralrimd  3243  spcimegf  3537  spcegf  3539  spcimedv  3542  spc2gv  3547  spc3gv  3551  rspcimedv  3560  2reu1  3839  pwpw0  4757  sssn  4770  pwsnOLD  4842  ssiun  4988  ssiun2  4989  wefrc  5601  ssrel  5711  ssrelOLD  5712  dmcosseq  5901  relssres  5951  trin2  6050  ssrnres  6103  sossfld  6111  reuop  6218  frpoinsg  6268  wfisgOLD  6279  tron  6311  ordtri3or  6320  oneqmini  6339  fnun  6583  f1oun  6772  brprcneu  6801  brprcneuALT  6802  ssimaex  6892  chfnrn  6965  dffo4  7018  dffo5  7019  tpres  7115  fvclss  7154  isomin  7247  isofrlem  7250  isoselem  7251  fnoprabg  7438  tfisg  7746  nnsuc  7776  f1oweALT  7861  releldmdifi  7932  bropopvvv  7976  bropfvvvvlem  7977  frxp  8012  poxp  8014  fnse  8019  poseq  8023  mpoxopynvov0g  8078  issmo2  8228  smores  8231  smogt  8246  rdglim2  8311  tz7.48lem  8320  tz7.49  8324  swoer  8577  qsss  8616  domtriord  8966  findcard  9006  findcard2  9007  pssnn  9011  ssfiALT  9017  pssnnOLD  9108  findcard2OLD  9127  findcard3  9128  findcard3OLD  9129  frfi  9131  dffi3  9266  supmo  9287  infmo  9330  inf3lem4  9466  frinsg  9586  carddom2  9812  fidomtri2  9829  pm54.43  9836  infpwfien  9897  alephordi  9909  cardaleph  9924  carduniima  9931  cardinfima  9932  alephval3  9945  dfac5lem4  9961  dfac5  9963  dfac2b  9965  kmlem2  9986  cflm  10085  cfslb2n  10103  cfsmolem  10105  isf32lem9  10196  axcc4  10274  domtriomlem  10277  zorn2lem4  10334  zorn2lem6  10336  fpwwe2lem10  10475  fpwwe2lem11  10476  inttsk  10609  inar1  10610  intgru  10649  ingru  10650  indpi  10742  nqpr  10849  ltaddpr  10869  ltexprlem1  10871  ltexprlem5  10875  reclem2pr  10883  reclem4pr  10885  negn0  11483  zmulcl  12448  uzm1  12695  uzwo  12730  xmullem2  13078  icoshft  13284  difreicc  13295  fzouzsplit  13501  ssfzoulel  13560  seqf1olem1  13841  seqf1olem2  13842  hashge2el2difr  14273  hashtpg  14277  reusq0  15250  modfsummod  15582  incexclem  15624  sqrt2irr  16034  dvds2lem  16054  dvdslelem  16094  oddnn02np1  16133  divalglem8  16185  dfgcd2  16330  2mulprm  16472  ge2nprmge4  16480  euclemma  16492  iserodd  16610  ramcl  16804  setsstruct  16951  mreiincl  17379  joinfval  18165  meetfval  18179  dirge  18395  sylow2alem1  19295  efgredlemb  19424  kerf1ghm  20059  rmodislmodlem  20270  lbspss  20424  lspsneu  20465  lspsnat  20487  lspsncv0  20488  opsrtoslem2  21343  distop  22225  epttop  22239  isclo2  22319  restdis  22409  subbascn  22485  cnrest2  22517  cnpresti  22519  isnrm2  22589  cmpsublem  22630  cmpcld  22633  dfconn2  22650  t1connperf  22667  1stcrest  22684  lly1stc  22727  uptx  22856  txcn  22857  prdstopn  22859  txconn  22920  cmphaushmeo  23031  fbasrn  23115  csdfil  23125  trufil  23141  fclscf  23256  alexsubALTlem3  23280  alexsubALT  23282  haustsms2  23368  ovoliunlem1  24746  ovoliunnul  24751  volsup2  24849  coeaddlem  25490  plymul0or  25521  radcnv0  25655  wilthlem3  26299  chtub  26440  gausslemma2dlem1a  26593  2sqlem10  26656  pntpbnd1  26814  sltval2  26884  mptelee  27396  axeuclidlem  27463  axcontlem4  27468  elntg2  27486  uhgrissubgr  27775  finsumvtxdg2size  28050  wlkonl1iedg  28165  pthdivtx  28229  wlkiswwlksupgr2  28374  eucrct2eupth  28741  isch3  29735  shmodsi  29883  orthin  29940  h1datomi  30075  stcltr2i  30769  atom1d  30847  sumdmdii  30909  cdj3lem1  30928  disjpreima  31054  lmxrge0  32038  dmvlsiga  32233  sibfof  32443  bnj600  33034  bnj1018g  33078  bnj1018  33079  bnj1173  33117  bnj1174  33118  pthisspthorcycl  33225  subgrwlk  33229  cusgracyclt3v  33253  erdszelem9  33296  cvmlift2lem1  33399  satfvsucsuc  33462  sat1el2xp  33476  fmla0xp  33480  fundmpss  33868  noetalem1  34014  bday1s  34095  outsideofrflx  34499  nn0prpwlem  34581  ivthALT  34594  fnessref  34616  neibastop2lem  34619  tailfb  34636  bj-axtd  34846  bj-nfimt  34889  bj-nfdt0  34947  bj-nnfand  35001  bj-sbievw2  35099  bj-2upleq  35270  bj-restn0  35338  icorempo  35599  isbasisrelowllem2  35604  rdgellim  35624  rdgssun  35626  pibt2  35665  wl-lem-moexsb  35800  matunitlindflem1  35850  poimirlem3  35857  poimirlem4  35858  poimirlem29  35883  mblfinlem3  35893  itg2addnclem3  35907  cover2  35949  fdc  35980  nninfnub  35986  equivtotbnd  36013  prdstotbnd  36029  cntotbnd  36031  ablo4pnp  36115  isdrngo3  36194  crngohomfo  36241  intidl  36264  or32dd  36329  iss2  36582  refressn  36682  eldisjlem19  37049  prtlem18  37116  prter2  37120  lsat0cv  37272  lfl1  37309  lkreqN  37409  atlrelat1  37560  pmaple  38001  pmapsub  38008  pclclN  38131  pclfinN  38140  osumcllem4N  38199  pexmidlem1N  38210  cdleme7ga  38488  lcfl7N  39741  isdomn4  40401  rtprmirr  40568  ss2iundf  41506  brtrclfv2  41574  ismnushort  42158  nzss  42174  3impexpbicom  42338  alrim3con13v  42392  tratrb  42395  onfrALTlem3  42403  onfrALTlem2  42405  onfrALTlem1  42407  trsspwALT2  42678  trsspwALT3  42679  or2expropbi  44798  afv2orxorb  44990  lswn0  45166  ich2exprop  45193  prproropf1olem4  45228  paireqne  45233  reupr  45244  lighneallem4b  45331  sbgoldbwt  45499  sbgoldbst  45500  sbgoldbalt  45503  isomuspgrlem1  45549  isomuspgrlem2d  45553  isupwlkg  45569  2zrngamgm  45767  fldivexpfllog2  46181  line2ylem  46367  fdomne0  46447