Theorem imbitrrdi 255

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbitrrdi.1	⊢ (𝜑 → (𝜓 → 𝜒))
imbitrrdi.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
imbitrrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem imbitrrdi

Step	Hyp	Ref	Expression
1		imbitrrdi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imbitrrdi.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	biimpri 231	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 36	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr4g  299  nic-ax  1706  sbequ1  2287  dfmoeu  2563  2moswapv  2657  mopick2  2665  2moswap  2672  2eu6  2684  necon3d  2980  necon1d  2981  ralrimd  3271  spcimegf  3518  spcegf  3550  spcimedv  3553  spc2gv  3558  spc3gv  3562  rspcimedv  3571  2reu1  3849  sssn  4785  pwpw0  4834  ssiun  5008  ssiun2  5009  replem  5245  wefrc  5650  ssrel  5765  dmcosseq  5968  dmcosseqOLD  5969  relssres  6024  trin2  6130  ssrnres  6183  sossfld  6191  reuop  6317  frpoinsg  6367  tron  6406  ordtri3or  6416  oneqmini  6437  fnun  6678  f1oun  6869  brprcneu  6901  brprcneuALT  6902  ssimaex  6996  chfnrn  7074  dffo4  7130  dffo5  7131  tpres  7233  fvclss  7271  isomin  7371  isofrlem  7374  isoselem  7375  fnoprabg  7569  mpt3fvd  7715  tfisg  7892  nnsuc  7922  f1oweALT  8011  releldmdifi  8084  bropopvvv  8129  bropfvvvvlem  8130  frxp  8168  poxp  8170  fnse  8180  poseq  8205  mpoxopynvov0g  8262  issmo2  8388  smores  8391  smogt  8406  rdglim2  8471  onelfvnef1  8480  tz7.48lemOLD  8482  tz7.49  8486  swoer  8780  qsss  8827  domtriord  9173  findcard  9210  findcard2  9211  pssnn  9215  ssfiALT  9220  findcard3  9305  frfi  9307  dffi3  9453  supmo  9474  infmo  9519  inf3lem4  9662  frinsg  9785  carddom2  10088  fidomtri2  10105  pm54.43  10112  infpwfien  10171  alephordi  10183  cardaleph  10198  carduniima  10205  cardinfima  10206  alephval3  10219  dfac5lem4  10235  dfac5  10237  dfac2b  10239  kmlem2  10260  cflm  10357  cfslb2n  10376  cfsmolem  10378  isf32lem9  10469  axcc4  10547  domtriomlem  10550  zorn2lem4  10607  zorn2lem6  10609  fpwwe2lem10  10755  fpwwe2lem11  10756  inttsk  10889  inar1  10890  intgru  10929  ingru  10930  indpi  11022  nqpr  11129  ltaddpr  11149  ltexprlem1  11151  ltexprlem5  11155  reclem2pr  11163  reclem4pr  11165  negn0  11775  zmulcl  12775  uzm1  13029  uzwo  13068  xmullem2  13425  icoshft  13634  difreicc  13645  fzouzsplit  13859  ssfzoulel  13925  seqf1olem1  14214  seqf1olem2  14215  hashge2el2difr  14656  hashtpg  14660  reusq0  15664  modfsummod  15993  incexclem  16037  sqrt2irr  16449  dvds2lem  16470  dvdslelem  16511  oddnn02np1  16550  divalglem8  16602  dfgcd2  16751  2mulprm  16900  ge2nprmge4  16909  euclemma  16921  iserodd  17045  ramcl  17239  setsstruct  17386  mreiincl  17798  joinfval  18577  meetfval  18591  dirge  18809  chnccat  18832  kerf1ghm  19493  sylow2alem1  19864  efgredlemb  19993  crngrhmfo  20759  isdomn4  21000  isdrng5  21041  rmodislmodlem  21237  lbspss  21390  lspsneu  21434  lspsnat  21456  lspsncv0  21457  opsrtoslem2  22398  matunitlindflem1  23027  distop  23346  epttop  23360  isclo2  23439  restdis  23529  subbascn  23605  cnrest2  23637  cnpresti  23639  isnrm2  23709  cmpsublem  23750  cmpcld  23753  dfconn2  23770  t1connperf  23787  1stcrest  23804  lly1stc  23848  uptx  23977  txcn  23978  prdstopn  23980  txconn  24041  cmphaushmeo  24152  fbasrn  24236  csdfil  24246  trufil  24262  fclscf  24377  alexsubALTlem3  24401  alexsubALT  24403  haustsms2  24489  ovoliunlem1  25856  ovoliunnul  25861  volsup2  25959  coeaddlem  26601  plymul0or  26632  radcnv0  26776  rtprmirr  27121  wilthlem3  27430  chtub  27572  gausslemma2dlem1a  27725  2sqlem10  27788  pntpbnd1  27946  ltsval2  28046  noetalem1  28131  bday1  28233  mpteleeOLD  29506  axeuclidlem  29573  axcontlem4  29578  elntg2  29596  uhgrissubgr  29889  finsumvtxdg2size  30164  wlkonl1iedg  30277  subgrwlk  30302  pthdivtx  30345  pthisspthorcycl  30423  wlkiswwlksupgr2  30499  eucrct2eupth  30879  isch3  31876  shmodsi  32024  orthin  32081  h1datomi  32216  stcltr2i  32910  atom1d  32988  sumdmdii  33050  cdj3lem1  33069  disjpreima  33253  lmxrge0  34667  dmvlsiga  34844  sibfof  35055  bnj600  35632  bnj1018g  35676  bnj1018  35677  bnj1173  35715  bnj1174  35716  rmo6  35793  fnfvintima  35799  trssfihf  35832  trssfihfregs  35917  karddom  35942  kardsdom  35943  dfk12  36025  dfk22  36026  dfk32  36027  onvf1odlem2  36045  onvf1odlem4  36047  onprcf1acwevdlem1  36058  cusgracyclt3v  36091  erdszelem9  36144  ptpconn  36178  cvmlift2lem1  36247  satfvsucsuc  36310  sat1el2xp  36324  fmla0xp  36328  3jcadALT  36632  fundmpss  36723  outsideofrflx  37083  nn0prpwlem  37301  ivthALT  37314  fnessref  37336  neibastop2lem  37339  tailfb  37356  bj-axtd  37655  bj-nfimt  37713  bj-nfdt0  37788  bj-nnfand  37848  bj-sbievw2  37949  bj-2upleq  38116  bj-restn0  38215  icorempo  38479  isbasisrelowllem2  38484  rdgellim  38504  rdgssun  38506  pibt2  38545  wl-lem-moexsb  38705  poimirlem3  38746  poimirlem4  38747  poimirlem29  38772  mblfinlem3  38782  itg2addnclem3  38796  cover2  38854  fdc  38882  nninfnub  38888  equivtotbnd  38915  prdstotbnd  38931  cntotbnd  38933  ablo4pnp  39017  isdrngo3  39096  crngohomfo  39143  intidl  39166  or32dd  39229  iss2  39479  refressn  39668  eldisjlem19  40048  prtlem18  40137  prter2  40141  lsat0cv  40293  lfl1  40330  lkreqN  40430  atlrelat1  40581  pmapsub  41028  pclclN  41151  pclfinN  41160  osumcllem4N  41219  pexmidlem1N  41230  cdleme7ga  41508  lcfl7N  42761  eu6w  43891  dflim5  44534  omabs2  44537  ss2iundf  44862  brtrclfv2  44930  ismnushort  45488  nzss  45504  3impexpbicom  45665  alrim3con13v  45718  tratrb  45721  onfrALTlem3  45729  onfrALTlem2  45731  onfrALTlem1  45733  trsspwALT2  46003  trsspwALT3  46004  relpmin  46148  relpfrlem  46149  trfr  46158  or2expropbi  48319  afv2orxorb  48513  lswn0  48741  ich2exprop  48768  prproropf1olem4  48803  paireqne  48808  reupr  48819  lighneallem4b  48909  sbgoldbwt  49090  sbgoldbst  49091  sbgoldbalt  49094  cycldlenngric  49241  isupwlkg  49450  2zrngamgm  49557  fldivexpfllog2  49892  line2ylem  50078  fdomne0  50176