Theorem syl6ibr 252

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. In the process of being renamed to imbitrrdi 251. (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:  difreicc  13461  fzouzsplit  13667  ssfzoulel  13726  seqf1olem1  14007  seqf1olem2  14008  hashge2el2difr  14442  hashtpg  14446  reusq0  15409  modfsummod  15740  incexclem  15782  sqrt2irr  16192  dvds2lem  16212  dvdslelem  16252  oddnn02np1  16291  divalglem8  16343  dfgcd2  16488  2mulprm  16630  ge2nprmge4  16638  euclemma  16650  iserodd  16768  ramcl  16962  setsstruct  17109  mreiincl  17540  joinfval  18326  meetfval  18340  dirge  18556  sylow2alem1  19485  efgredlemb  19614  kerf1ghm  20282  rmodislmodlem  20539  lbspss  20693  lspsneu  20736  lspsnat  20758  lspsncv0  20759  isdomn4  20918  opsrtoslem2  21617  distop  22498  epttop  22512  isclo2  22592  restdis  22682  subbascn  22758  cnrest2  22790  cnpresti  22792  isnrm2  22862  cmpsublem  22903  cmpcld  22906  dfconn2  22923  t1connperf  22940  1stcrest  22957  lly1stc  23000  uptx  23129  txcn  23130  prdstopn  23132  txconn  23193  cmphaushmeo  23304  fbasrn  23388  csdfil  23398  trufil  23414  fclscf  23529  alexsubALTlem3  23553  alexsubALT  23555  haustsms2  23641  ovoliunlem1  25019  ovoliunnul  25024  volsup2  25122  coeaddlem  25763  plymul0or  25794  radcnv0  25928  wilthlem3  26574  chtub  26715  gausslemma2dlem1a  26868  2sqlem10  26931  pntpbnd1  27089  sltval2  27159  noetalem1  27244  bday1s  27332  mptelee  28153  axeuclidlem  28220  axcontlem4  28225  elntg2  28243  uhgrissubgr  28532  finsumvtxdg2size  28807  wlkonl1iedg  28922  pthdivtx  28986  wlkiswwlksupgr2  29131  eucrct2eupth  29498  isch3  30494  shmodsi  30642  orthin  30699  h1datomi  30834  stcltr2i  31528  atom1d  31606  sumdmdii  31668  cdj3lem1  31687  disjpreima  31815  lmxrge0  32932  dmvlsiga  33127  sibfof  33339  bnj600  33930  bnj1018g  33974  bnj1018  33975  bnj1173  34013  bnj1174  34014  pthisspthorcycl  34119  subgrwlk  34123  cusgracyclt3v  34147  erdszelem9  34190  cvmlift2lem1  34293  satfvsucsuc  34356  sat1el2xp  34370  fmla0xp  34374  fundmpss  34738  outsideofrflx  35099  nn0prpwlem  35207  ivthALT  35220  fnessref  35242  neibastop2lem  35245  tailfb  35262  bj-axtd  35472  bj-nfimt  35515  bj-nfdt0  35573  bj-nnfand  35627  bj-sbievw2  35725  bj-2upleq  35893  bj-restn0  35971  icorempo  36232  isbasisrelowllem2  36237  rdgellim  36257  rdgssun  36259  pibt2  36298  wl-lem-moexsb  36433  matunitlindflem1  36484  poimirlem3  36491  poimirlem4  36492  poimirlem29  36517  mblfinlem3  36527  itg2addnclem3  36541  cover2  36583  fdc  36613  nninfnub  36619  equivtotbnd  36646  prdstotbnd  36662  cntotbnd  36664  ablo4pnp  36748  isdrngo3  36827  crngohomfo  36874  intidl  36897  or32dd  36962  iss2  37213  refressn  37313  eldisjlem19  37680  prtlem18  37747  prter2  37751  lsat0cv  37903  lfl1  37940  lkreqN  38040  atlrelat1  38191  pmaple  38632  pmapsub  38639  pclclN  38762  pclfinN  38771  osumcllem4N  38830  pexmidlem1N  38841  cdleme7ga  39119  lcfl7N  40372  rtprmirr  41237  dflim5  42079  omabs2  42082  ss2iundf  42410  brtrclfv2  42478  ismnushort  43060  nzss  43076  3impexpbicom  43240  alrim3con13v  43294  tratrb  43297  onfrALTlem3  43305  onfrALTlem2  43307  onfrALTlem1  43309  trsspwALT2  43580  trsspwALT3  43581  or2expropbi  45744  afv2orxorb  45936  lswn0  46112  ich2exprop  46139  prproropf1olem4  46174  paireqne  46179  reupr  46190  lighneallem4b  46277  sbgoldbwt  46445  sbgoldbst  46446  sbgoldbalt  46449  isomuspgrlem1  46495  isomuspgrlem2d  46499  isupwlkg  46515  2zrngamgm  46837  fldivexpfllog2  47251  line2ylem  47437  fdomne0  47516