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  1673  sbequ1  2249  dfmoeu  2529  2moswapv  2622  mopick2  2630  2moswap  2637  2eu6  2650  necon3d  2946  necon1d  2947  ralrimd  3242  spcimegf  3517  spcegf  3558  spcimedv  3561  spc2gv  3566  spc3gv  3570  rspcimedv  3579  2reu1  3860  pwpw0  4777  sssn  4790  ssiun  5010  ssiun2  5011  wefrc  5632  ssrel  5745  ssrelOLD  5746  dmcosseq  5940  dmcosseqOLD  5941  relssres  5993  trin2  6096  ssrnres  6151  sossfld  6159  reuop  6266  frpoinsg  6316  tron  6355  ordtri3or  6364  oneqmini  6385  fnun  6632  f1oun  6819  brprcneu  6848  brprcneuALT  6849  ssimaex  6946  chfnrn  7021  dffo4  7075  dffo5  7076  tpres  7175  fvclss  7215  isomin  7312  isofrlem  7315  isoselem  7316  fnoprabg  7512  tfisg  7830  nnsuc  7860  f1oweALT  7951  releldmdifi  8024  bropopvvv  8069  bropfvvvvlem  8070  frxp  8105  poxp  8107  fnse  8112  poseq  8137  mpoxopynvov0g  8193  issmo2  8318  smores  8321  smogt  8336  rdglim2  8400  tz7.48lem  8409  tz7.49  8413  swoer  8702  qsss  8749  domtriord  9087  findcard  9127  findcard2  9128  pssnn  9132  ssfiALT  9138  findcard3  9229  findcard3OLD  9230  frfi  9232  dffi3  9382  supmo  9403  infmo  9448  inf3lem4  9584  frinsg  9704  carddom2  9930  fidomtri2  9947  pm54.43  9954  infpwfien  10015  alephordi  10027  cardaleph  10042  carduniima  10049  cardinfima  10050  alephval3  10063  dfac5lem4  10079  dfac5lem4OLD  10081  dfac5  10082  dfac2b  10084  kmlem2  10105  cflm  10203  cfslb2n  10221  cfsmolem  10223  isf32lem9  10314  axcc4  10392  domtriomlem  10395  zorn2lem4  10452  zorn2lem6  10454  fpwwe2lem10  10593  fpwwe2lem11  10594  inttsk  10727  inar1  10728  intgru  10767  ingru  10768  indpi  10860  nqpr  10967  ltaddpr  10987  ltexprlem1  10989  ltexprlem5  10993  reclem2pr  11001  reclem4pr  11003  negn0  11607  zmulcl  12582  uzm1  12831  uzwo  12870  xmullem2  13225  icoshft  13434  difreicc  13445  fzouzsplit  13655  ssfzoulel  13721  seqf1olem1  14006  seqf1olem2  14007  hashge2el2difr  14446  hashtpg  14450  reusq0  15431  modfsummod  15760  incexclem  15802  sqrt2irr  16217  dvds2lem  16238  dvdslelem  16279  oddnn02np1  16318  divalglem8  16370  dfgcd2  16516  2mulprm  16663  ge2nprmge4  16671  euclemma  16683  iserodd  16806  ramcl  17000  setsstruct  17146  mreiincl  17557  joinfval  18332  meetfval  18346  dirge  18562  kerf1ghm  19179  sylow2alem1  19547  efgredlemb  19676  isdomn4  20625  rmodislmodlem  20835  lbspss  20989  lspsneu  21033  lspsnat  21055  lspsncv0  21056  opsrtoslem2  21963  distop  22882  epttop  22896  isclo2  22975  restdis  23065  subbascn  23141  cnrest2  23173  cnpresti  23175  isnrm2  23245  cmpsublem  23286  cmpcld  23289  dfconn2  23306  t1connperf  23323  1stcrest  23340  lly1stc  23383  uptx  23512  txcn  23513  prdstopn  23515  txconn  23576  cmphaushmeo  23687  fbasrn  23771  csdfil  23781  trufil  23797  fclscf  23912  alexsubALTlem3  23936  alexsubALT  23938  haustsms2  24024  ovoliunlem1  25403  ovoliunnul  25408  volsup2  25506  coeaddlem  26154  plymul0or  26188  radcnv0  26325  rtprmirr  26670  wilthlem3  26980  chtub  27123  gausslemma2dlem1a  27276  2sqlem10  27339  pntpbnd1  27497  sltval2  27568  noetalem1  27653  bday1s  27743  mptelee  28822  axeuclidlem  28889  axcontlem4  28894  elntg2  28912  uhgrissubgr  29202  finsumvtxdg2size  29478  wlkonl1iedg  29593  pthdivtx  29657  pthisspthorcycl  29732  wlkiswwlksupgr2  29807  eucrct2eupth  30174  isch3  31170  shmodsi  31318  orthin  31375  h1datomi  31510  stcltr2i  32204  atom1d  32282  sumdmdii  32344  cdj3lem1  32363  disjpreima  32513  lmxrge0  33942  dmvlsiga  34119  sibfof  34331  bnj600  34909  bnj1018g  34953  bnj1018  34954  bnj1173  34992  bnj1174  34993  onvf1odlem2  35091  onvf1odlem4  35093  subgrwlk  35119  cusgracyclt3v  35143  erdszelem9  35186  cvmlift2lem1  35289  satfvsucsuc  35352  sat1el2xp  35366  fmla0xp  35370  3jcadALT  35674  fundmpss  35754  outsideofrflx  36115  nn0prpwlem  36310  ivthALT  36323  fnessref  36345  neibastop2lem  36348  tailfb  36365  bj-axtd  36582  bj-nfimt  36626  bj-nfdt0  36683  bj-nnfand  36737  bj-sbievw2  36834  bj-2upleq  37000  bj-restn0  37078  icorempo  37339  isbasisrelowllem2  37344  rdgellim  37364  rdgssun  37366  pibt2  37405  wl-lem-moexsb  37556  matunitlindflem1  37610  poimirlem3  37617  poimirlem4  37618  poimirlem29  37643  mblfinlem3  37653  itg2addnclem3  37667  cover2  37709  fdc  37739  nninfnub  37745  equivtotbnd  37772  prdstotbnd  37788  cntotbnd  37790  ablo4pnp  37874  isdrngo3  37953  crngohomfo  38000  intidl  38023  or32dd  38088  iss2  38326  refressn  38434  eldisjlem19  38802  prtlem18  38870  prter2  38874  lsat0cv  39026  lfl1  39063  lkreqN  39163  atlrelat1  39314  pmaple  39755  pmapsub  39762  pclclN  39885  pclfinN  39894  osumcllem4N  39953  pexmidlem1N  39964  cdleme7ga  40242  lcfl7N  41495  eu6w  42664  dflim5  43318  omabs2  43321  ss2iundf  43648  brtrclfv2  43716  ismnushort  44290  nzss  44306  3impexpbicom  44470  alrim3con13v  44523  tratrb  44526  onfrALTlem3  44534  onfrALTlem2  44536  onfrALTlem1  44538  trsspwALT2  44808  trsspwALT3  44809  relpmin  44942  relpfrlem  44943  trfr  44952  or2expropbi  47035  afv2orxorb  47229  lswn0  47445  ich2exprop  47472  prproropf1olem4  47507  paireqne  47512  reupr  47523  lighneallem4b  47610  sbgoldbwt  47778  sbgoldbst  47779  sbgoldbalt  47782  cycldlenngric  47928  isupwlkg  48125  2zrngamgm  48233  fldivexpfllog2  48554  line2ylem  48740  fdomne0  48838