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  2536  2moswapv  2629  mopick2  2637  2moswap  2644  2eu6  2657  necon3d  2954  necon1d  2955  ralrimd  3251  spcimegf  3535  spcegf  3576  spcimedv  3579  spc2gv  3584  spc3gv  3588  rspcimedv  3597  2reu1  3877  pwpw0  4794  sssn  4807  ssiun  5027  ssiun2  5028  wefrc  5653  ssrel  5766  ssrelOLD  5767  dmcosseq  5961  dmcosseqOLD  5962  relssres  6014  trin2  6117  ssrnres  6172  sossfld  6180  reuop  6287  frpoinsg  6337  wfisgOLD  6348  tron  6380  ordtri3or  6389  oneqmini  6410  fnun  6657  f1oun  6842  brprcneu  6871  brprcneuALT  6872  ssimaex  6969  chfnrn  7044  dffo4  7098  dffo5  7099  tpres  7198  fvclss  7238  isomin  7335  isofrlem  7338  isoselem  7339  fnoprabg  7535  tfisg  7854  nnsuc  7884  f1oweALT  7976  releldmdifi  8049  bropopvvv  8094  bropfvvvvlem  8095  frxp  8130  poxp  8132  fnse  8137  poseq  8162  mpoxopynvov0g  8218  issmo2  8368  smores  8371  smogt  8386  rdglim2  8451  tz7.48lem  8460  tz7.49  8464  swoer  8755  qsss  8797  domtriord  9142  findcard  9182  findcard2  9183  pssnn  9187  ssfiALT  9193  findcard3  9295  findcard3OLD  9296  frfi  9298  dffi3  9448  supmo  9469  infmo  9514  inf3lem4  9650  frinsg  9770  carddom2  9996  fidomtri2  10013  pm54.43  10020  infpwfien  10081  alephordi  10093  cardaleph  10108  carduniima  10115  cardinfima  10116  alephval3  10129  dfac5lem4  10145  dfac5lem4OLD  10147  dfac5  10148  dfac2b  10150  kmlem2  10171  cflm  10269  cfslb2n  10287  cfsmolem  10289  isf32lem9  10380  axcc4  10458  domtriomlem  10461  zorn2lem4  10518  zorn2lem6  10520  fpwwe2lem10  10659  fpwwe2lem11  10660  inttsk  10793  inar1  10794  intgru  10833  ingru  10834  indpi  10926  nqpr  11033  ltaddpr  11053  ltexprlem1  11055  ltexprlem5  11059  reclem2pr  11067  reclem4pr  11069  negn0  11671  zmulcl  12646  uzm1  12895  uzwo  12932  xmullem2  13286  icoshft  13495  difreicc  13506  fzouzsplit  13716  ssfzoulel  13781  seqf1olem1  14064  seqf1olem2  14065  hashge2el2difr  14504  hashtpg  14508  reusq0  15486  modfsummod  15815  incexclem  15857  sqrt2irr  16272  dvds2lem  16293  dvdslelem  16333  oddnn02np1  16372  divalglem8  16424  dfgcd2  16570  2mulprm  16717  ge2nprmge4  16725  euclemma  16737  iserodd  16860  ramcl  17054  setsstruct  17200  mreiincl  17613  joinfval  18388  meetfval  18402  dirge  18618  kerf1ghm  19235  sylow2alem1  19603  efgredlemb  19732  isdomn4  20681  rmodislmodlem  20891  lbspss  21045  lspsneu  21089  lspsnat  21111  lspsncv0  21112  opsrtoslem2  22019  distop  22938  epttop  22952  isclo2  23031  restdis  23121  subbascn  23197  cnrest2  23229  cnpresti  23231  isnrm2  23301  cmpsublem  23342  cmpcld  23345  dfconn2  23362  t1connperf  23379  1stcrest  23396  lly1stc  23439  uptx  23568  txcn  23569  prdstopn  23571  txconn  23632  cmphaushmeo  23743  fbasrn  23827  csdfil  23837  trufil  23853  fclscf  23968  alexsubALTlem3  23992  alexsubALT  23994  haustsms2  24080  ovoliunlem1  25460  ovoliunnul  25465  volsup2  25563  coeaddlem  26211  plymul0or  26245  radcnv0  26382  rtprmirr  26727  wilthlem3  27037  chtub  27180  gausslemma2dlem1a  27333  2sqlem10  27396  pntpbnd1  27554  sltval2  27625  noetalem1  27710  bday1s  27800  mptelee  28879  axeuclidlem  28946  axcontlem4  28951  elntg2  28969  uhgrissubgr  29259  finsumvtxdg2size  29535  wlkonl1iedg  29650  pthdivtx  29714  pthisspthorcycl  29789  wlkiswwlksupgr2  29864  eucrct2eupth  30231  isch3  31227  shmodsi  31375  orthin  31432  h1datomi  31567  stcltr2i  32261  atom1d  32339  sumdmdii  32401  cdj3lem1  32420  disjpreima  32570  lmxrge0  33988  dmvlsiga  34165  sibfof  34377  bnj600  34955  bnj1018g  34999  bnj1018  35000  bnj1173  35038  bnj1174  35039  subgrwlk  35159  cusgracyclt3v  35183  erdszelem9  35226  cvmlift2lem1  35329  satfvsucsuc  35392  sat1el2xp  35406  fmla0xp  35410  3jcadALT  35714  fundmpss  35789  outsideofrflx  36150  nn0prpwlem  36345  ivthALT  36358  fnessref  36380  neibastop2lem  36383  tailfb  36400  bj-axtd  36617  bj-nfimt  36661  bj-nfdt0  36718  bj-nnfand  36772  bj-sbievw2  36869  bj-2upleq  37035  bj-restn0  37113  icorempo  37374  isbasisrelowllem2  37379  rdgellim  37399  rdgssun  37401  pibt2  37440  wl-lem-moexsb  37591  matunitlindflem1  37645  poimirlem3  37652  poimirlem4  37653  poimirlem29  37678  mblfinlem3  37688  itg2addnclem3  37702  cover2  37744  fdc  37774  nninfnub  37780  equivtotbnd  37807  prdstotbnd  37823  cntotbnd  37825  ablo4pnp  37909  isdrngo3  37988  crngohomfo  38035  intidl  38058  or32dd  38123  iss2  38367  refressn  38466  eldisjlem19  38833  prtlem18  38900  prter2  38904  lsat0cv  39056  lfl1  39093  lkreqN  39193  atlrelat1  39344  pmaple  39785  pmapsub  39792  pclclN  39915  pclfinN  39924  osumcllem4N  39983  pexmidlem1N  39994  cdleme7ga  40272  lcfl7N  41525  eu6w  42674  dflim5  43328  omabs2  43331  ss2iundf  43658  brtrclfv2  43726  ismnushort  44300  nzss  44316  3impexpbicom  44480  alrim3con13v  44533  tratrb  44536  onfrALTlem3  44544  onfrALTlem2  44546  onfrALTlem1  44548  trsspwALT2  44818  trsspwALT3  44819  relpmin  44952  relpfrlem  44953  trfr  44962  or2expropbi  47043  afv2orxorb  47237  lswn0  47438  ich2exprop  47465  prproropf1olem4  47500  paireqne  47505  reupr  47516  lighneallem4b  47603  sbgoldbwt  47771  sbgoldbst  47772  sbgoldbalt  47775  cycldlenngric  47921  isupwlkg  48092  2zrngamgm  48200  fldivexpfllog2  48525  line2ylem  48711  fdomne0  48808