Theorem syl6ibr 252

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  2531  2moswapv  2626  mopick2  2634  2moswap  2641  2eu6  2653  necon3d  2962  necon1d  2963  ralrimd  3262  spcimegf  3581  spcegf  3583  spcimedv  3586  spc2gv  3591  spc3gv  3595  rspcimedv  3604  2reu1  3891  pwpw0  4816  sssn  4829  pwsnOLD  4901  ssiun  5049  ssiun2  5050  wefrc  5670  ssrel  5781  ssrelOLD  5782  dmcosseq  5971  relssres  6021  trin2  6122  ssrnres  6175  sossfld  6183  reuop  6290  frpoinsg  6342  wfisgOLD  6353  tron  6385  ordtri3or  6394  oneqmini  6414  fnun  6661  f1oun  6850  brprcneu  6879  brprcneuALT  6880  ssimaex  6974  chfnrn  7048  dffo4  7102  dffo5  7103  tpres  7199  fvclss  7238  isomin  7331  isofrlem  7334  isoselem  7335  fnoprabg  7528  tfisg  7840  nnsuc  7870  f1oweALT  7956  releldmdifi  8028  bropopvvv  8073  bropfvvvvlem  8074  frxp  8109  poxp  8111  fnse  8116  poseq  8141  mpoxopynvov0g  8196  issmo2  8346  smores  8349  smogt  8364  rdglim2  8429  tz7.48lem  8438  tz7.49  8442  swoer  8730  qsss  8769  domtriord  9120  findcard  9160  findcard2  9161  pssnn  9165  ssfiALT  9171  pssnnOLD  9262  findcard2OLD  9281  findcard3  9282  findcard3OLD  9283  frfi  9285  dffi3  9423  supmo  9444  infmo  9487  inf3lem4  9623  frinsg  9743  carddom2  9969  fidomtri2  9986  pm54.43  9993  infpwfien  10054  alephordi  10066  cardaleph  10081  carduniima  10088  cardinfima  10089  alephval3  10102  dfac5lem4  10118  dfac5  10120  dfac2b  10122  kmlem2  10143  cflm  10242  cfslb2n  10260  cfsmolem  10262  isf32lem9  10353  axcc4  10431  domtriomlem  10434  zorn2lem4  10491  zorn2lem6  10493  fpwwe2lem10  10632  fpwwe2lem11  10633  inttsk  10766  inar1  10767  intgru  10806  ingru  10807  indpi  10899  nqpr  11006  ltaddpr  11026  ltexprlem1  11028  ltexprlem5  11032  reclem2pr  11040  reclem4pr  11042  negn0  11640  zmulcl  12608  uzm1  12857  uzwo  12892  xmullem2  13241  icoshft  13447  difreicc  13458  fzouzsplit  13664  ssfzoulel  13723  seqf1olem1  14004  seqf1olem2  14005  hashge2el2difr  14439  hashtpg  14443  reusq0  15406  modfsummod  15737  incexclem  15779  sqrt2irr  16189  dvds2lem  16209  dvdslelem  16249  oddnn02np1  16288  divalglem8  16340  dfgcd2  16485  2mulprm  16627  ge2nprmge4  16635  euclemma  16647  iserodd  16765  ramcl  16959  setsstruct  17106  mreiincl  17537  joinfval  18323  meetfval  18337  dirge  18553  sylow2alem1  19480  efgredlemb  19609  kerf1ghm  20275  rmodislmodlem  20532  lbspss  20686  lspsneu  20729  lspsnat  20751  lspsncv0  20752  isdomn4  20911  opsrtoslem2  21609  distop  22490  epttop  22504  isclo2  22584  restdis  22674  subbascn  22750  cnrest2  22782  cnpresti  22784  isnrm2  22854  cmpsublem  22895  cmpcld  22898  dfconn2  22915  t1connperf  22932  1stcrest  22949  lly1stc  22992  uptx  23121  txcn  23122  prdstopn  23124  txconn  23185  cmphaushmeo  23296  fbasrn  23380  csdfil  23390  trufil  23406  fclscf  23521  alexsubALTlem3  23545  alexsubALT  23547  haustsms2  23633  ovoliunlem1  25011  ovoliunnul  25016  volsup2  25114  coeaddlem  25755  plymul0or  25786  radcnv0  25920  wilthlem3  26564  chtub  26705  gausslemma2dlem1a  26858  2sqlem10  26921  pntpbnd1  27079  sltval2  27149  noetalem1  27234  bday1s  27322  mptelee  28143  axeuclidlem  28210  axcontlem4  28215  elntg2  28233  uhgrissubgr  28522  finsumvtxdg2size  28797  wlkonl1iedg  28912  pthdivtx  28976  wlkiswwlksupgr2  29121  eucrct2eupth  29488  isch3  30482  shmodsi  30630  orthin  30687  h1datomi  30822  stcltr2i  31516  atom1d  31594  sumdmdii  31656  cdj3lem1  31675  disjpreima  31803  lmxrge0  32921  dmvlsiga  33116  sibfof  33328  bnj600  33919  bnj1018g  33963  bnj1018  33964  bnj1173  34002  bnj1174  34003  pthisspthorcycl  34108  subgrwlk  34112  cusgracyclt3v  34136  erdszelem9  34179  cvmlift2lem1  34282  satfvsucsuc  34345  sat1el2xp  34359  fmla0xp  34363  fundmpss  34727  outsideofrflx  35088  nn0prpwlem  35196  ivthALT  35209  fnessref  35231  neibastop2lem  35234  tailfb  35251  bj-axtd  35461  bj-nfimt  35504  bj-nfdt0  35562  bj-nnfand  35616  bj-sbievw2  35714  bj-2upleq  35882  bj-restn0  35960  icorempo  36221  isbasisrelowllem2  36226  rdgellim  36246  rdgssun  36248  pibt2  36287  wl-lem-moexsb  36422  matunitlindflem1  36473  poimirlem3  36480  poimirlem4  36481  poimirlem29  36506  mblfinlem3  36516  itg2addnclem3  36530  cover2  36572  fdc  36602  nninfnub  36608  equivtotbnd  36635  prdstotbnd  36651  cntotbnd  36653  ablo4pnp  36737  isdrngo3  36816  crngohomfo  36863  intidl  36886  or32dd  36951  iss2  37202  refressn  37302  eldisjlem19  37669  prtlem18  37736  prter2  37740  lsat0cv  37892  lfl1  37929  lkreqN  38029  atlrelat1  38180  pmaple  38621  pmapsub  38628  pclclN  38751  pclfinN  38760  osumcllem4N  38819  pexmidlem1N  38830  cdleme7ga  39108  lcfl7N  40361  rtprmirr  41234  dflim5  42065  omabs2  42068  ss2iundf  42396  brtrclfv2  42464  ismnushort  43046  nzss  43062  3impexpbicom  43226  alrim3con13v  43280  tratrb  43283  onfrALTlem3  43291  onfrALTlem2  43293  onfrALTlem1  43295  trsspwALT2  43566  trsspwALT3  43567  or2expropbi  45731  afv2orxorb  45923  lswn0  46099  ich2exprop  46126  prproropf1olem4  46161  paireqne  46166  reupr  46177  lighneallem4b  46264  sbgoldbwt  46432  sbgoldbst  46433  sbgoldbalt  46436  isomuspgrlem1  46482  isomuspgrlem2d  46486  isupwlkg  46502  2zrngamgm  46791  fldivexpfllog2  47205  line2ylem  47391  fdomne0  47470