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  296  nic-ax  1676  sbequ1  2241  dfmoeu  2537  2moswapv  2632  mopick2  2640  2moswap  2647  2eu6  2659  necon3d  2965  necon1d  2966  ralrimd  3144  spcimegf  3530  spcegf  3532  spcimedv  3535  spc2gv  3540  spc3gv  3544  rspcimedv  3553  2reu1  3831  pwpw0  4747  sssn  4760  pwsnOLD  4833  ssiun  4977  ssiun2  4978  wefrc  5584  ssrel  5694  ssrelOLD  5695  dmcosseq  5885  relssres  5935  trin2  6033  ssrnres  6086  sossfld  6094  reuop  6200  frpoinsg  6250  wfisgOLD  6261  tron  6293  ordtri3or  6302  oneqmini  6321  fnun  6554  f1oun  6744  brprcneu  6773  brprcneuALT  6774  ssimaex  6862  chfnrn  6935  dffo4  6988  dffo5  6989  tpres  7085  fvclss  7124  isomin  7217  isofrlem  7220  isoselem  7221  fnoprabg  7406  nnsuc  7739  f1oweALT  7824  releldmdifi  7895  bropopvvv  7939  bropfvvvvlem  7940  frxp  7976  poxp  7978  fnse  7983  mpoxopynvov0g  8039  issmo2  8189  smores  8192  smogt  8207  rdglim2  8272  tz7.48lem  8281  tz7.49  8285  swoer  8537  qsss  8576  domtriord  8919  findcard  8955  findcard2  8956  pssnn  8960  ssfiALT  8966  pssnnOLD  9049  findcard2OLD  9065  findcard3  9066  frfi  9068  dffi3  9199  supmo  9220  infmo  9263  inf3lem4  9398  frinsg  9518  carddom2  9744  fidomtri2  9761  pm54.43  9768  infpwfien  9827  alephordi  9839  cardaleph  9854  carduniima  9861  cardinfima  9862  alephval3  9875  dfac5lem4  9891  dfac5  9893  dfac2b  9895  kmlem2  9916  cflm  10015  cfslb2n  10033  cfsmolem  10035  isf32lem9  10126  axcc4  10204  domtriomlem  10207  zorn2lem4  10264  zorn2lem6  10266  fpwwe2lem10  10405  fpwwe2lem11  10406  inttsk  10539  inar1  10540  intgru  10579  ingru  10580  indpi  10672  nqpr  10779  ltaddpr  10799  ltexprlem1  10801  ltexprlem5  10805  reclem2pr  10813  reclem4pr  10815  negn0  11413  zmulcl  12378  uzm1  12625  uzwo  12660  xmullem2  13008  icoshft  13214  difreicc  13225  fzouzsplit  13431  ssfzoulel  13490  seqf1olem1  13771  seqf1olem2  13772  hashge2el2difr  14204  hashtpg  14208  reusq0  15183  modfsummod  15515  incexclem  15557  sqrt2irr  15967  dvds2lem  15987  dvdslelem  16027  oddnn02np1  16066  divalglem8  16118  dfgcd2  16263  2mulprm  16407  ge2nprmge4  16415  euclemma  16427  iserodd  16545  ramcl  16739  setsstruct  16886  mreiincl  17314  joinfval  18100  meetfval  18114  dirge  18330  sylow2alem1  19231  efgredlemb  19361  kerf1ghm  19996  rmodislmodlem  20199  lbspss  20353  lspsneu  20394  lspsnat  20416  lspsncv0  20417  opsrtoslem2  21272  distop  22154  epttop  22168  isclo2  22248  restdis  22338  subbascn  22414  cnrest2  22446  cnpresti  22448  isnrm2  22518  cmpsublem  22559  cmpcld  22562  dfconn2  22579  t1connperf  22596  1stcrest  22613  lly1stc  22656  uptx  22785  txcn  22786  prdstopn  22788  txconn  22849  cmphaushmeo  22960  fbasrn  23044  csdfil  23054  trufil  23070  fclscf  23185  alexsubALTlem3  23209  alexsubALT  23211  haustsms2  23297  ovoliunlem1  24675  ovoliunnul  24680  volsup2  24778  coeaddlem  25419  plymul0or  25450  radcnv0  25584  wilthlem3  26228  chtub  26369  gausslemma2dlem1a  26522  2sqlem10  26585  pntpbnd1  26743  mptelee  27272  axeuclidlem  27339  axcontlem4  27344  elntg2  27362  uhgrissubgr  27651  finsumvtxdg2size  27926  wlkonl1iedg  28042  pthdivtx  28106  wlkiswwlksupgr2  28251  eucrct2eupth  28618  isch3  29612  shmodsi  29760  orthin  29817  h1datomi  29952  stcltr2i  30646  atom1d  30724  sumdmdii  30786  cdj3lem1  30805  disjpreima  30932  lmxrge0  31911  dmvlsiga  32106  sibfof  32316  bnj600  32908  bnj1018g  32952  bnj1018  32953  bnj1173  32991  bnj1174  32992  pthisspthorcycl  33099  subgrwlk  33103  cusgracyclt3v  33127  erdszelem9  33170  cvmlift2lem1  33273  satfvsucsuc  33336  sat1el2xp  33350  fmla0xp  33354  fundmpss  33749  tfisg  33795  poseq  33811  sltval2  33868  noetalem1  33953  bday1s  34034  outsideofrflx  34438  nn0prpwlem  34520  ivthALT  34533  fnessref  34555  neibastop2lem  34558  tailfb  34575  bj-axtd  34785  bj-nfimt  34828  bj-nfdt0  34886  bj-nnfand  34940  bj-sbievw2  35039  bj-2upleq  35211  bj-restn0  35270  icorempo  35531  isbasisrelowllem2  35536  rdgellim  35556  rdgssun  35558  pibt2  35597  wl-lem-moexsb  35732  matunitlindflem1  35782  poimirlem3  35789  poimirlem4  35790  poimirlem29  35815  mblfinlem3  35825  itg2addnclem3  35839  cover2  35881  fdc  35912  nninfnub  35918  equivtotbnd  35945  prdstotbnd  35961  cntotbnd  35963  ablo4pnp  36047  isdrngo3  36126  crngohomfo  36173  intidl  36196  or32dd  36261  iss2  36486  prtlem18  36898  prter2  36902  lsat0cv  37054  lfl1  37091  lkreqN  37191  atlrelat1  37342  pmaple  37782  pmapsub  37789  pclclN  37912  pclfinN  37921  osumcllem4N  37980  pexmidlem1N  37991  cdleme7ga  38269  lcfl7N  39522  isdomn4  40179  rtprmirr  40354  ss2iundf  41274  brtrclfv2  41342  ismnushort  41926  nzss  41942  3impexpbicom  42106  alrim3con13v  42160  tratrb  42163  onfrALTlem3  42171  onfrALTlem2  42173  onfrALTlem1  42175  trsspwALT2  42446  trsspwALT3  42447  or2expropbi  44539  afv2orxorb  44731  lswn0  44907  ich2exprop  44934  prproropf1olem4  44969  paireqne  44974  reupr  44985  lighneallem4b  45072  sbgoldbwt  45240  sbgoldbst  45241  sbgoldbalt  45244  isomuspgrlem1  45290  isomuspgrlem2d  45294  isupwlkg  45310  2zrngamgm  45508  fldivexpfllog2  45922  line2ylem  46108  fdomne0  46188