Theorem imbitrrdi 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, 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 228	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr4g  296  nic-ax  1674  sbequ1  2253  dfmoeu  2533  2moswapv  2626  mopick2  2634  2moswap  2641  2eu6  2654  necon3d  2950  necon1d  2951  ralrimd  3238  spcimegf  3505  spcegf  3543  spcimedv  3546  spc2gv  3551  spc3gv  3555  rspcimedv  3564  2reu1  3844  pwpw0  4764  sssn  4777  ssiun  4997  ssiun2  4998  wefrc  5613  ssrel  5727  dmcosseq  5921  dmcosseqOLD  5922  dmcosseqOLDOLD  5923  relssres  5975  trin2  6074  ssrnres  6130  sossfld  6138  reuop  6245  frpoinsg  6295  tron  6334  ordtri3or  6343  oneqmini  6364  fnun  6600  f1oun  6787  brprcneu  6818  brprcneuALT  6819  ssimaex  6913  chfnrn  6988  dffo4  7042  dffo5  7043  tpres  7141  fvclss  7181  isomin  7277  isofrlem  7280  isoselem  7281  fnoprabg  7475  tfisg  7790  nnsuc  7820  f1oweALT  7910  releldmdifi  7983  bropopvvv  8026  bropfvvvvlem  8027  frxp  8062  poxp  8064  fnse  8069  poseq  8094  mpoxopynvov0g  8150  issmo2  8275  smores  8278  smogt  8293  rdglim2  8357  tz7.48lem  8366  tz7.49  8370  swoer  8659  qsss  8706  domtriord  9043  findcard  9080  findcard2  9081  pssnn  9085  ssfiALT  9090  findcard3  9174  frfi  9176  dffi3  9322  supmo  9343  infmo  9388  inf3lem4  9528  frinsg  9651  carddom2  9877  fidomtri2  9894  pm54.43  9901  infpwfien  9960  alephordi  9972  cardaleph  9987  carduniima  9994  cardinfima  9995  alephval3  10008  dfac5lem4  10024  dfac5lem4OLD  10026  dfac5  10027  dfac2b  10029  kmlem2  10050  cflm  10148  cfslb2n  10166  cfsmolem  10168  isf32lem9  10259  axcc4  10337  domtriomlem  10340  zorn2lem4  10397  zorn2lem6  10399  fpwwe2lem10  10538  fpwwe2lem11  10539  inttsk  10672  inar1  10673  intgru  10712  ingru  10713  indpi  10805  nqpr  10912  ltaddpr  10932  ltexprlem1  10934  ltexprlem5  10938  reclem2pr  10946  reclem4pr  10948  negn0  11553  zmulcl  12527  uzm1  12772  uzwo  12811  xmullem2  13166  icoshft  13375  difreicc  13386  fzouzsplit  13596  ssfzoulel  13662  seqf1olem1  13950  seqf1olem2  13951  hashge2el2difr  14390  hashtpg  14394  reusq0  15374  modfsummod  15703  incexclem  15745  sqrt2irr  16160  dvds2lem  16181  dvdslelem  16222  oddnn02np1  16261  divalglem8  16313  dfgcd2  16459  2mulprm  16606  ge2nprmge4  16614  euclemma  16626  iserodd  16749  ramcl  16943  setsstruct  17089  mreiincl  17500  joinfval  18279  meetfval  18293  dirge  18511  chnccat  18534  kerf1ghm  19161  sylow2alem1  19531  efgredlemb  19660  isdomn4  20633  rmodislmodlem  20864  lbspss  21018  lspsneu  21062  lspsnat  21084  lspsncv0  21085  opsrtoslem2  21992  distop  22911  epttop  22925  isclo2  23004  restdis  23094  subbascn  23170  cnrest2  23202  cnpresti  23204  isnrm2  23274  cmpsublem  23315  cmpcld  23318  dfconn2  23335  t1connperf  23352  1stcrest  23369  lly1stc  23412  uptx  23541  txcn  23542  prdstopn  23544  txconn  23605  cmphaushmeo  23716  fbasrn  23800  csdfil  23810  trufil  23826  fclscf  23941  alexsubALTlem3  23965  alexsubALT  23967  haustsms2  24053  ovoliunlem1  25431  ovoliunnul  25436  volsup2  25534  coeaddlem  26182  plymul0or  26216  radcnv0  26353  rtprmirr  26698  wilthlem3  27008  chtub  27151  gausslemma2dlem1a  27304  2sqlem10  27367  pntpbnd1  27525  sltval2  27596  noetalem1  27681  bday1s  27776  mpteleeOLD  28875  axeuclidlem  28942  axcontlem4  28947  elntg2  28965  uhgrissubgr  29255  finsumvtxdg2size  29531  wlkonl1iedg  29644  pthdivtx  29707  pthisspthorcycl  29782  wlkiswwlksupgr2  29857  eucrct2eupth  30227  isch3  31223  shmodsi  31371  orthin  31428  h1datomi  31563  stcltr2i  32257  atom1d  32335  sumdmdii  32397  cdj3lem1  32416  disjpreima  32566  lmxrge0  33986  dmvlsiga  34163  sibfof  34374  bnj600  34952  bnj1018g  34996  bnj1018  34997  bnj1173  35035  bnj1174  35036  trssfir1om  35143  trssfir1omregs  35153  onvf1odlem2  35169  onvf1odlem4  35171  subgrwlk  35197  cusgracyclt3v  35221  erdszelem9  35264  cvmlift2lem1  35367  satfvsucsuc  35430  sat1el2xp  35444  fmla0xp  35448  3jcadALT  35752  fundmpss  35832  outsideofrflx  36192  nn0prpwlem  36387  ivthALT  36400  fnessref  36422  neibastop2lem  36425  tailfb  36442  bj-axtd  36659  bj-nfimt  36703  bj-nfdt0  36760  bj-nnfand  36814  bj-sbievw2  36911  bj-2upleq  37077  bj-restn0  37155  icorempo  37416  isbasisrelowllem2  37421  rdgellim  37441  rdgssun  37443  pibt2  37482  wl-lem-moexsb  37633  matunitlindflem1  37676  poimirlem3  37683  poimirlem4  37684  poimirlem29  37709  mblfinlem3  37719  itg2addnclem3  37733  cover2  37775  fdc  37805  nninfnub  37811  equivtotbnd  37838  prdstotbnd  37854  cntotbnd  37856  ablo4pnp  37940  isdrngo3  38019  crngohomfo  38066  intidl  38089  or32dd  38154  iss2  38396  refressn  38565  eldisjlem19  38928  prtlem18  38996  prter2  39000  lsat0cv  39152  lfl1  39189  lkreqN  39289  atlrelat1  39440  pmapsub  39887  pclclN  40010  pclfinN  40019  osumcllem4N  40078  pexmidlem1N  40089  cdleme7ga  40367  lcfl7N  41620  eu6w  42794  dflim5  43446  omabs2  43449  ss2iundf  43776  brtrclfv2  43844  ismnushort  44418  nzss  44434  3impexpbicom  44597  alrim3con13v  44650  tratrb  44653  onfrALTlem3  44661  onfrALTlem2  44663  onfrALTlem1  44665  trsspwALT2  44935  trsspwALT3  44936  relpmin  45069  relpfrlem  45070  trfr  45079  or2expropbi  47158  afv2orxorb  47352  lswn0  47568  ich2exprop  47595  prproropf1olem4  47630  paireqne  47635  reupr  47646  lighneallem4b  47733  sbgoldbwt  47901  sbgoldbst  47902  sbgoldbalt  47905  cycldlenngric  48052  isupwlkg  48261  2zrngamgm  48369  fldivexpfllog2  48690  line2ylem  48876  fdomne0  48974