Theorem syl6ibr 254

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 230	. 2 ⊢ (𝜒 → 𝜃)
4	1, 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:  3imtr4g  298  nic-ax  1674  sbequ1  2249  dfmoeu  2618  euimOLD  2702  2moswapv  2714  mopick2  2722  2moswap  2729  2eu6  2742  necon3d  3039  necon1d  3040  ralrimd  3220  spcimegf  3591  spcegf  3593  spcimedv  3596  spc2gv  3603  spc3gv  3607  rspcimedv  3616  2reu1  3883  pwpw0  4748  sssn  4761  pwsnOLD  4833  ssiun  4972  ssiun2  4973  wefrc  5551  ssrel  5659  dmcosseq  5846  relssres  5895  trin2  5985  ssrnres  6037  sossfld  6045  reuop  6146  wfisg  6185  tron  6216  ordtri3or  6225  oneqmini  6244  fnun  6465  f1oun  6636  brprcneu  6664  ssimaex  6750  chfnrn  6821  dffo4  6871  dffo5  6872  tpres  6965  fvclss  7003  isomin  7092  isofrlem  7095  isoselem  7096  fnoprabg  7277  nnsuc  7599  f1oweALT  7675  releldmdifi  7746  bropopvvv  7787  bropfvvvvlem  7788  frxp  7822  poxp  7824  fnse  7829  mpoxopynvov0g  7882  issmo2  7988  smores  7991  smogt  8006  rdglim2  8070  tz7.48lem  8079  tz7.49  8083  swoer  8321  qsss  8360  domtriord  8665  pssnn  8738  ssfi  8740  findcard  8759  findcard2  8760  findcard3  8763  frfi  8765  dffi3  8897  supmo  8918  infmo  8961  inf3lem4  9096  carddom2  9408  fidomtri2  9425  pm54.43  9431  infpwfien  9490  alephordi  9502  cardaleph  9517  carduniima  9524  cardinfima  9525  alephval3  9538  dfac5lem4  9554  dfac5  9556  dfac2b  9558  kmlem2  9579  cflm  9674  cfslb2n  9692  cfsmolem  9694  isf32lem9  9785  axcc4  9863  domtriomlem  9866  zorn2lem4  9923  zorn2lem6  9925  fpwwe2lem11  10064  fpwwe2lem12  10065  inttsk  10198  inar1  10199  intgru  10238  ingru  10239  indpi  10331  nqpr  10438  ltaddpr  10458  ltexprlem1  10460  ltexprlem5  10464  reclem2pr  10472  reclem4pr  10474  negn0  11071  zmulcl  12034  uzm1  12279  uzwo  12314  xmullem2  12661  icoshft  12862  difreicc  12873  fzouzsplit  13075  ssfzoulel  13134  seqf1olem1  13412  seqf1olem2  13413  hashge2el2difr  13842  hashtpg  13846  reusq0  14824  modfsummod  15151  incexclem  15193  sqrt2irr  15604  dvds2lem  15624  dvdslelem  15661  oddnn02np1  15699  divalglem8  15753  dfgcd2  15896  2mulprm  16039  ge2nprmge4  16047  euclemma  16059  iserodd  16174  ramcl  16367  setsstruct  16525  mreiincl  16869  joinfval  17613  meetfval  17627  dirge  17849  sylow2alem1  18744  efgredlemb  18874  kerf1ghm  19499  kerf1hrmOLD  19500  rmodislmodlem  19703  lbspss  19856  lspsneu  19897  lspsnat  19919  lspsncv0  19920  opsrtoslem2  20267  distop  21605  epttop  21619  isclo2  21698  restdis  21788  subbascn  21864  cnrest2  21896  cnpresti  21898  isnrm2  21968  cmpsublem  22009  cmpcld  22012  dfconn2  22029  t1connperf  22046  1stcrest  22063  lly1stc  22106  uptx  22235  txcn  22236  prdstopn  22238  txconn  22299  cmphaushmeo  22410  fbasrn  22494  csdfil  22504  trufil  22520  fclscf  22635  alexsubALTlem3  22659  alexsubALT  22661  haustsms2  22747  ovoliunlem1  24105  ovoliunnul  24110  volsup2  24208  coeaddlem  24841  plymul0or  24872  radcnv0  25006  wilthlem3  25649  chtub  25790  gausslemma2dlem1a  25943  2sqlem10  26006  pntpbnd1  26164  mptelee  26683  axeuclidlem  26750  axcontlem4  26755  elntg2  26773  uhgrissubgr  27059  finsumvtxdg2size  27334  wlkonl1iedg  27449  pthdivtx  27512  wlkiswwlksupgr2  27657  eucrct2eupth  28026  isch3  29020  shmodsi  29168  orthin  29225  h1datomi  29360  stcltr2i  30054  atom1d  30132  sumdmdii  30194  cdj3lem1  30213  disjpreima  30336  lmxrge0  31197  dmvlsiga  31390  sibfof  31600  bnj600  32193  bnj1018g  32237  bnj1018  32238  bnj1173  32276  bnj1174  32277  pthisspthorcycl  32377  subgrwlk  32381  cusgracyclt3v  32405  erdszelem9  32448  cvmlift2lem1  32551  satfvsucsuc  32614  sat1el2xp  32628  fmla0xp  32632  fundmpss  33011  tfisg  33057  frpoinsg  33083  frinsg  33089  poseq  33097  sltval2  33165  outsideofrflx  33590  nn0prpwlem  33672  ivthALT  33685  fnessref  33707  neibastop2lem  33710  tailfb  33727  bj-axtd  33930  bj-nfimt  33973  bj-nfdt0  34031  bj-nnfand  34080  bj-sbievw2  34172  bj-2upleq  34326  bj-restn0  34383  icorempo  34634  isbasisrelowllem2  34639  rdgellim  34659  rdgssun  34661  pibt2  34700  wl-lem-moexsb  34806  matunitlindflem1  34890  poimirlem3  34897  poimirlem4  34898  poimirlem29  34923  mblfinlem3  34933  itg2addnclem3  34947  cover2  34991  fdc  35022  nninfnub  35028  equivtotbnd  35058  prdstotbnd  35074  cntotbnd  35076  ablo4pnp  35160  isdrngo3  35239  crngohomfo  35286  intidl  35309  or32dd  35374  iss2  35603  prtlem18  36015  prter2  36019  lsat0cv  36171  lfl1  36208  lkreqN  36308  atlrelat1  36459  pmaple  36899  pmapsub  36906  pclclN  37029  pclfinN  37038  osumcllem4N  37097  pexmidlem1N  37108  cdleme7ga  37386  lcfl7N  38639  rtprmirr  39201  ss2iundf  40011  brtrclfv2  40079  nzss  40656  3impexpbicom  40820  alrim3con13v  40874  tratrb  40877  onfrALTlem3  40885  onfrALTlem2  40887  onfrALTlem1  40889  trsspwALT2  41160  trsspwALT3  41161  or2expropbi  43276  afv2orxorb  43434  lswn0  43611  ich2exprop  43640  prproropf1olem4  43675  paireqne  43680  reupr  43691  lighneallem4b  43781  sbgoldbwt  43949  sbgoldbst  43950  sbgoldbalt  43953  isomuspgrlem1  43999  isomuspgrlem2d  44003  isupwlkg  44019  2zrngamgm  44217  fldivexpfllog2  44632  line2ylem  44745