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 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr4g  299  nic-ax  1696  sbequ1  2286  dfmoeu  2565  2moswapv  2659  mopick2  2667  2moswap  2674  2eu6  2686  necon3d  2981  necon1d  2982  ralrimd  3270  spcimegf  3522  spcegf  3554  spcimedv  3557  spc2gv  3562  spc3gv  3566  rspcimedv  3575  2reu1  3853  pwpw0  4774  sssn  4787  ssiun  5007  ssiun2  5008  replem  5243  wefrc  5646  ssrel  5760  dmcosseq  5959  dmcosseqOLD  5960  relssres  6012  trin2  6114  ssrnres  6168  sossfld  6176  reuop  6284  frpoinsg  6334  tron  6373  ordtri3or  6382  oneqmini  6403  fnun  6639  f1oun  6830  brprcneu  6861  brprcneuALT  6862  ssimaex  6956  chfnrn  7034  dffo4  7088  dffo5  7089  tpres  7189  fvclss  7229  isomin  7325  isofrlem  7328  isoselem  7329  fnoprabg  7523  tfisg  7838  nnsuc  7868  f1oweALT  7957  releldmdifi  8030  bropopvvv  8073  bropfvvvvlem  8074  frxp  8110  poxp  8112  fnse  8117  poseq  8142  mpoxopynvov0g  8198  issmo2  8324  smores  8327  smogt  8342  rdglim2  8407  tz7.48lem  8416  tz7.49  8420  swoer  8714  qsss  8761  domtriord  9099  findcard  9136  findcard2  9137  pssnn  9141  ssfiALT  9146  findcard3  9231  frfi  9233  dffi3  9379  supmo  9400  infmo  9445  inf3lem4  9588  frinsg  9711  carddom2  9951  fidomtri2  9968  pm54.43  9975  infpwfien  10034  alephordi  10046  cardaleph  10061  carduniima  10068  cardinfima  10069  alephval3  10082  dfac5lem4  10098  dfac5  10100  dfac2b  10102  kmlem2  10123  cflm  10221  cfslb2n  10240  cfsmolem  10242  isf32lem9  10333  axcc4  10411  domtriomlem  10414  zorn2lem4  10471  zorn2lem6  10473  fpwwe2lem10  10613  fpwwe2lem11  10614  inttsk  10747  inar1  10748  intgru  10787  ingru  10788  indpi  10880  nqpr  10987  ltaddpr  11007  ltexprlem1  11009  ltexprlem5  11013  reclem2pr  11021  reclem4pr  11023  negn0  11631  zmulcl  12634  uzm1  12887  uzwo  12926  xmullem2  13282  icoshft  13491  difreicc  13502  fzouzsplit  13714  ssfzoulel  13780  seqf1olem1  14068  seqf1olem2  14069  hashge2el2difr  14508  hashtpg  14512  reusq0  15506  modfsummod  15836  incexclem  15880  sqrt2irr  16295  dvds2lem  16316  dvdslelem  16357  oddnn02np1  16396  divalglem8  16448  dfgcd2  16594  2mulprm  16741  ge2nprmge4  16750  euclemma  16762  iserodd  16885  ramcl  17079  setsstruct  17226  mreiincl  17638  joinfval  18417  meetfval  18431  dirge  18649  chnccat  18672  kerf1ghm  19308  sylow2alem1  19678  efgredlemb  19807  isdomn4  20791  rmodislmodlem  21019  lbspss  21172  lspsneu  21216  lspsnat  21238  lspsncv0  21239  opsrtoslem2  22167  distop  23113  epttop  23127  isclo2  23206  restdis  23296  subbascn  23372  cnrest2  23404  cnpresti  23406  isnrm2  23476  cmpsublem  23517  cmpcld  23520  dfconn2  23537  t1connperf  23554  1stcrest  23571  lly1stc  23614  uptx  23743  txcn  23744  prdstopn  23746  txconn  23807  cmphaushmeo  23918  fbasrn  24002  csdfil  24012  trufil  24028  fclscf  24143  alexsubALTlem3  24167  alexsubALT  24169  haustsms2  24255  ovoliunlem1  25622  ovoliunnul  25627  volsup2  25725  coeaddlem  26367  plymul0or  26400  radcnv0  26537  rtprmirr  26883  wilthlem3  27192  chtub  27334  gausslemma2dlem1a  27487  2sqlem10  27550  pntpbnd1  27708  ltsval2  27778  noetalem1  27863  bday1  27965  mpteleeOLD  29154  axeuclidlem  29221  axcontlem4  29226  elntg2  29244  uhgrissubgr  29534  finsumvtxdg2size  29809  wlkonl1iedg  29922  pthdivtx  29985  pthisspthorcycl  30060  wlkiswwlksupgr2  30135  eucrct2eupth  30505  isch3  31502  shmodsi  31650  orthin  31707  h1datomi  31842  stcltr2i  32536  atom1d  32614  sumdmdii  32676  cdj3lem1  32695  disjpreima  32839  lmxrge0  34259  dmvlsiga  34436  sibfof  34647  bnj600  35224  bnj1018g  35268  bnj1018  35269  bnj1173  35307  bnj1174  35308  trssfir1om  35419  trssfir1omregs  35444  onvf1odlem2  35459  onvf1odlem4  35461  subgrwlk  35495  cusgracyclt3v  35519  erdszelem9  35562  cvmlift2lem1  35665  satfvsucsuc  35728  sat1el2xp  35742  fmla0xp  35746  3jcadALT  36050  fundmpss  36130  outsideofrflx  36490  nn0prpwlem  36695  ivthALT  36708  fnessref  36730  neibastop2lem  36733  tailfb  36750  mh-inf3f1  36914  bj-axtd  37049  bj-nfimt  37107  bj-nfdt0  37182  bj-nnfand  37242  bj-sbievw2  37343  bj-2upleq  37509  bj-restn0  37592  icorempo  37857  isbasisrelowllem2  37862  rdgellim  37882  rdgssun  37884  pibt2  37923  wl-lem-moexsb  38083  matunitlindflem1  38127  poimirlem3  38134  poimirlem4  38135  poimirlem29  38160  mblfinlem3  38170  itg2addnclem3  38184  cover2  38226  fdc  38256  nninfnub  38262  equivtotbnd  38289  prdstotbnd  38305  cntotbnd  38307  ablo4pnp  38391  isdrngo3  38470  crngohomfo  38517  intidl  38540  or32dd  38605  iss2  38855  refressn  39044  eldisjlem19  39424  prtlem18  39513  prter2  39517  lsat0cv  39669  lfl1  39706  lkreqN  39806  atlrelat1  39957  pmapsub  40404  pclclN  40527  pclfinN  40536  osumcllem4N  40595  pexmidlem1N  40606  cdleme7ga  40884  lcfl7N  42137  eu6w  43270  dflim5  43918  omabs2  43921  ss2iundf  44247  brtrclfv2  44315  ismnushort  44875  nzss  44891  3impexpbicom  45054  alrim3con13v  45107  tratrb  45110  onfrALTlem3  45118  onfrALTlem2  45120  onfrALTlem1  45122  trsspwALT2  45392  trsspwALT3  45393  relpmin  45526  relpfrlem  45527  trfr  45536  or2expropbi  47626  afv2orxorb  47820  lswn0  48048  ich2exprop  48075  prproropf1olem4  48110  paireqne  48115  reupr  48126  lighneallem4b  48216  sbgoldbwt  48397  sbgoldbst  48398  sbgoldbalt  48401  cycldlenngric  48548  isupwlkg  48757  2zrngamgm  48865  fldivexpfllog2  49196  line2ylem  49382  fdomne0  49479