Theorem imbitrrdi 251

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr4g  296  nic-ax  1668  sbequ1  2233  dfmoeu  2525  2moswapv  2620  mopick2  2628  2moswap  2635  2eu6  2647  necon3d  2956  necon1d  2957  ralrimd  3256  spcimegf  3575  spcegf  3577  spcimedv  3580  spc2gv  3585  spc3gv  3589  rspcimedv  3598  2reu1  3887  pwpw0  4812  sssn  4825  ssiun  5043  ssiun2  5044  wefrc  5666  ssrel  5778  ssrelOLD  5779  dmcosseq  5970  relssres  6020  trin2  6123  ssrnres  6176  sossfld  6184  reuop  6291  frpoinsg  6343  wfisgOLD  6354  tron  6386  ordtri3or  6395  oneqmini  6415  fnun  6662  f1oun  6852  brprcneu  6881  brprcneuALT  6882  ssimaex  6977  chfnrn  7052  dffo4  7107  dffo5  7108  tpres  7207  fvclss  7245  isomin  7339  isofrlem  7342  isoselem  7343  fnoprabg  7537  tfisg  7852  nnsuc  7882  f1oweALT  7970  releldmdifi  8043  bropopvvv  8089  bropfvvvvlem  8090  frxp  8125  poxp  8127  fnse  8132  poseq  8157  mpoxopynvov0g  8213  issmo2  8363  smores  8366  smogt  8381  rdglim2  8446  tz7.48lem  8455  tz7.49  8459  swoer  8748  qsss  8788  domtriord  9139  findcard  9179  findcard2  9180  pssnn  9184  ssfiALT  9190  pssnnOLD  9281  findcard2OLD  9300  findcard3  9301  findcard3OLD  9302  frfi  9304  dffi3  9446  supmo  9467  infmo  9510  inf3lem4  9646  frinsg  9766  carddom2  9992  fidomtri2  10009  pm54.43  10016  infpwfien  10077  alephordi  10089  cardaleph  10104  carduniima  10111  cardinfima  10112  alephval3  10125  dfac5lem4  10141  dfac5  10143  dfac2b  10145  kmlem2  10166  cflm  10265  cfslb2n  10283  cfsmolem  10285  isf32lem9  10376  axcc4  10454  domtriomlem  10457  zorn2lem4  10514  zorn2lem6  10516  fpwwe2lem10  10655  fpwwe2lem11  10656  inttsk  10789  inar1  10790  intgru  10829  ingru  10830  indpi  10922  nqpr  11029  ltaddpr  11049  ltexprlem1  11051  ltexprlem5  11055  reclem2pr  11063  reclem4pr  11065  negn0  11665  zmulcl  12633  uzm1  12882  uzwo  12917  xmullem2  13268  icoshft  13474  difreicc  13485  fzouzsplit  13691  ssfzoulel  13750  seqf1olem1  14030  seqf1olem2  14031  hashge2el2difr  14466  hashtpg  14470  reusq0  15433  modfsummod  15764  incexclem  15806  sqrt2irr  16217  dvds2lem  16237  dvdslelem  16277  oddnn02np1  16316  divalglem8  16368  dfgcd2  16513  2mulprm  16655  ge2nprmge4  16663  euclemma  16675  iserodd  16795  ramcl  16989  setsstruct  17136  mreiincl  17567  joinfval  18356  meetfval  18370  dirge  18586  kerf1ghm  19192  sylow2alem1  19563  efgredlemb  19692  rmodislmodlem  20801  lbspss  20956  lspsneu  21000  lspsnat  21022  lspsncv0  21023  isdomn4  21238  opsrtoslem2  21987  distop  22885  epttop  22899  isclo2  22979  restdis  23069  subbascn  23145  cnrest2  23177  cnpresti  23179  isnrm2  23249  cmpsublem  23290  cmpcld  23293  dfconn2  23310  t1connperf  23327  1stcrest  23344  lly1stc  23387  uptx  23516  txcn  23517  prdstopn  23519  txconn  23580  cmphaushmeo  23691  fbasrn  23775  csdfil  23785  trufil  23801  fclscf  23916  alexsubALTlem3  23940  alexsubALT  23942  haustsms2  24028  ovoliunlem1  25418  ovoliunnul  25423  volsup2  25521  coeaddlem  26170  plymul0or  26202  radcnv0  26339  wilthlem3  26989  chtub  27132  gausslemma2dlem1a  27285  2sqlem10  27348  pntpbnd1  27506  sltval2  27576  noetalem1  27661  bday1s  27751  mptelee  28693  axeuclidlem  28760  axcontlem4  28765  elntg2  28783  uhgrissubgr  29075  finsumvtxdg2size  29351  wlkonl1iedg  29466  pthdivtx  29530  wlkiswwlksupgr2  29675  eucrct2eupth  30042  isch3  31038  shmodsi  31186  orthin  31243  h1datomi  31378  stcltr2i  32072  atom1d  32150  sumdmdii  32212  cdj3lem1  32231  disjpreima  32359  lmxrge0  33489  dmvlsiga  33684  sibfof  33896  bnj600  34486  bnj1018g  34530  bnj1018  34531  bnj1173  34569  bnj1174  34570  pthisspthorcycl  34674  subgrwlk  34678  cusgracyclt3v  34702  erdszelem9  34745  cvmlift2lem1  34848  satfvsucsuc  34911  sat1el2xp  34925  fmla0xp  34929  fundmpss  35298  outsideofrflx  35659  nn0prpwlem  35742  ivthALT  35755  fnessref  35777  neibastop2lem  35780  tailfb  35797  bj-axtd  36007  bj-nfimt  36050  bj-nfdt0  36108  bj-nnfand  36162  bj-sbievw2  36259  bj-2upleq  36427  bj-restn0  36505  icorempo  36766  isbasisrelowllem2  36771  rdgellim  36791  rdgssun  36793  pibt2  36832  wl-lem-moexsb  36970  matunitlindflem1  37024  poimirlem3  37031  poimirlem4  37032  poimirlem29  37057  mblfinlem3  37067  itg2addnclem3  37081  cover2  37123  fdc  37153  nninfnub  37159  equivtotbnd  37186  prdstotbnd  37202  cntotbnd  37204  ablo4pnp  37288  isdrngo3  37367  crngohomfo  37414  intidl  37437  or32dd  37502  iss2  37752  refressn  37852  eldisjlem19  38219  prtlem18  38286  prter2  38290  lsat0cv  38442  lfl1  38479  lkreqN  38579  atlrelat1  38730  pmaple  39171  pmapsub  39178  pclclN  39301  pclfinN  39310  osumcllem4N  39369  pexmidlem1N  39380  cdleme7ga  39658  lcfl7N  40911  rtprmirr  41828  dflim5  42681  omabs2  42684  ss2iundf  43012  brtrclfv2  43080  ismnushort  43661  nzss  43677  3impexpbicom  43841  alrim3con13v  43895  tratrb  43898  onfrALTlem3  43906  onfrALTlem2  43908  onfrALTlem1  43910  trsspwALT2  44181  trsspwALT3  44182  or2expropbi  46339  afv2orxorb  46531  lswn0  46707  ich2exprop  46734  prproropf1olem4  46769  paireqne  46774  reupr  46785  lighneallem4b  46872  sbgoldbwt  47040  sbgoldbst  47041  sbgoldbalt  47044  isupwlkg  47122  2zrngamgm  47230  fldivexpfllog2  47561  line2ylem  47747  fdomne0  47825