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  2285  dfmoeu  2562  2moswapv  2656  mopick2  2664  2moswap  2671  2eu6  2683  necon3d  2978  necon1d  2979  ralrimd  3269  spcimegf  3517  spcegf  3549  spcimedv  3552  spc2gv  3557  spc3gv  3561  rspcimedv  3570  2reu1  3848  pwpw0  4777  sssn  4790  ssiun  5009  ssiun2  5010  replem  5247  wefrc  5653  ssrel  5767  dmcosseq  5966  dmcosseqOLD  5967  relssres  6019  trin2  6121  ssrnres  6175  sossfld  6183  reuop  6295  frpoinsg  6345  tron  6384  ordtri3or  6394  oneqmini  6415  fnun  6650  f1oun  6841  brprcneu  6872  brprcneuALT  6873  ssimaex  6967  chfnrn  7045  dffo4  7100  dffo5  7101  tpres  7204  fvclss  7242  isomin  7342  isofrlem  7345  isoselem  7346  fnoprabg  7540  tfisg  7854  nnsuc  7884  f1oweALT  7973  releldmdifi  8046  bropopvvv  8091  bropfvvvvlem  8092  frxp  8128  poxp  8130  fnse  8135  poseq  8160  mpoxopynvov0g  8216  issmo2  8342  smores  8345  smogt  8360  rdglim2  8425  tz7.48lem  8434  tz7.49  8438  swoer  8732  qsss  8779  domtriord  9125  findcard  9162  findcard2  9163  pssnn  9167  ssfiALT  9172  findcard3  9257  frfi  9259  dffi3  9405  supmo  9426  infmo  9471  inf3lem4  9614  frinsg  9737  carddom2  9986  fidomtri2  10003  pm54.43  10010  infpwfien  10069  alephordi  10081  cardaleph  10096  carduniima  10103  cardinfima  10104  alephval3  10117  dfac5lem4  10133  dfac5  10135  dfac2b  10137  kmlem2  10158  cflm  10255  cfslb2n  10274  cfsmolem  10276  isf32lem9  10367  axcc4  10445  domtriomlem  10448  zorn2lem4  10505  zorn2lem6  10507  fpwwe2lem10  10653  fpwwe2lem11  10654  inttsk  10787  inar1  10788  intgru  10827  ingru  10828  indpi  10920  nqpr  11027  ltaddpr  11047  ltexprlem1  11049  ltexprlem5  11053  reclem2pr  11061  reclem4pr  11063  negn0  11671  zmulcl  12671  uzm1  12925  uzwo  12964  xmullem2  13321  icoshft  13530  difreicc  13541  fzouzsplit  13754  ssfzoulel  13820  seqf1olem1  14109  seqf1olem2  14110  hashge2el2difr  14550  hashtpg  14554  reusq0  15556  modfsummod  15885  incexclem  15929  sqrt2irr  16343  dvds2lem  16364  dvdslelem  16405  oddnn02np1  16444  divalglem8  16496  dfgcd2  16642  2mulprm  16789  ge2nprmge4  16798  euclemma  16810  iserodd  16933  ramcl  17127  setsstruct  17274  mreiincl  17686  joinfval  18465  meetfval  18479  dirge  18697  chnccat  18720  kerf1ghm  19380  sylow2alem1  19750  efgredlemb  19879  crngrhmfo  20643  isdomn4  20883  isdrng5  20923  rmodislmodlem  21119  lbspss  21272  lspsneu  21316  lspsnat  21338  lspsncv0  21339  opsrtoslem2  22278  matunitlindflem1  22907  distop  23226  epttop  23240  isclo2  23319  restdis  23409  subbascn  23485  cnrest2  23517  cnpresti  23519  isnrm2  23589  cmpsublem  23630  cmpcld  23633  dfconn2  23650  t1connperf  23667  1stcrest  23684  lly1stc  23728  uptx  23857  txcn  23858  prdstopn  23860  txconn  23921  cmphaushmeo  24032  fbasrn  24116  csdfil  24126  trufil  24142  fclscf  24257  alexsubALTlem3  24281  alexsubALT  24283  haustsms2  24369  ovoliunlem1  25736  ovoliunnul  25741  volsup2  25839  coeaddlem  26482  plymul0or  26515  radcnv0  26659  rtprmirr  27005  wilthlem3  27314  chtub  27456  gausslemma2dlem1a  27609  2sqlem10  27672  pntpbnd1  27830  ltsval2  27900  noetalem1  27985  bday1  28087  mpteleeOLD  29360  axeuclidlem  29427  axcontlem4  29432  elntg2  29450  uhgrissubgr  29743  finsumvtxdg2size  30018  wlkonl1iedg  30131  subgrwlk  30156  pthdivtx  30199  pthisspthorcycl  30277  wlkiswwlksupgr2  30353  eucrct2eupth  30733  isch3  31730  shmodsi  31878  orthin  31935  h1datomi  32070  stcltr2i  32764  atom1d  32842  sumdmdii  32904  cdj3lem1  32923  disjpreima  33065  lmxrge0  34470  dmvlsiga  34647  sibfof  34859  bnj600  35436  bnj1018g  35480  bnj1018  35481  bnj1173  35519  bnj1174  35520  fnfvintima  35599  trssfir1om  35629  trssfir1omregs  35670  karddom  35695  kardsdom  35696  onvf1odlem2  35709  onvf1odlem4  35711  cusgracyclt3v  35743  erdszelem9  35786  cvmlift2lem1  35889  satfvsucsuc  35952  sat1el2xp  35966  fmla0xp  35970  3jcadALT  36274  fundmpss  36354  outsideofrflx  36715  nn0prpwlem  36949  ivthALT  36962  fnessref  36984  neibastop2lem  36987  tailfb  37004  mh-inf3f1  37168  bj-axtd  37303  bj-nfimt  37361  bj-nfdt0  37436  bj-nnfand  37496  bj-sbievw2  37597  bj-2upleq  37764  bj-restn0  37848  icorempo  38113  isbasisrelowllem2  38118  rdgellim  38138  rdgssun  38140  pibt2  38179  wl-lem-moexsb  38339  poimirlem3  38380  poimirlem4  38381  poimirlem29  38406  mblfinlem3  38416  itg2addnclem3  38430  cover2  38473  fdc  38503  nninfnub  38509  equivtotbnd  38536  prdstotbnd  38552  cntotbnd  38554  ablo4pnp  38638  isdrngo3  38717  crngohomfo  38764  intidl  38787  or32dd  38850  iss2  39100  refressn  39289  eldisjlem19  39669  prtlem18  39758  prter2  39762  lsat0cv  39914  lfl1  39951  lkreqN  40051  atlrelat1  40202  pmapsub  40649  pclclN  40772  pclfinN  40781  osumcllem4N  40840  pexmidlem1N  40851  cdleme7ga  41129  lcfl7N  42382  eu6w  43530  dflim5  44178  omabs2  44181  ss2iundf  44507  brtrclfv2  44575  ismnushort  45133  nzss  45149  3impexpbicom  45311  alrim3con13v  45364  tratrb  45367  onfrALTlem3  45375  onfrALTlem2  45377  onfrALTlem1  45379  trsspwALT2  45649  trsspwALT3  45650  relpmin  45783  relpfrlem  45784  trfr  45793  or2expropbi  47930  afv2orxorb  48124  lswn0  48352  ich2exprop  48379  prproropf1olem4  48414  paireqne  48419  reupr  48430  lighneallem4b  48520  sbgoldbwt  48701  sbgoldbst  48702  sbgoldbalt  48705  cycldlenngric  48852  isupwlkg  49061  2zrngamgm  49168  fldivexpfllog2  49503  line2ylem  49689  fdomne0  49786