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  1675  sbequ1  2256  dfmoeu  2535  2moswapv  2629  mopick2  2637  2moswap  2644  2eu6  2657  necon3d  2953  necon1d  2954  ralrimd  3242  spcimegf  3496  spcegf  3534  spcimedv  3537  spc2gv  3542  spc3gv  3546  rspcimedv  3555  2reu1  3835  pwpw0  4756  sssn  4769  ssiun  4989  ssiun2  4990  replem  5223  wefrc  5625  ssrel  5739  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  relssres  5987  trin2  6086  ssrnres  6142  sossfld  6150  reuop  6257  frpoinsg  6307  tron  6346  ordtri3or  6355  oneqmini  6376  fnun  6612  f1oun  6799  brprcneu  6830  brprcneuALT  6831  ssimaex  6925  chfnrn  7001  dffo4  7055  dffo5  7056  tpres  7156  fvclss  7196  isomin  7292  isofrlem  7295  isoselem  7296  fnoprabg  7490  tfisg  7805  nnsuc  7835  f1oweALT  7925  releldmdifi  7998  bropopvvv  8040  bropfvvvvlem  8041  frxp  8076  poxp  8078  fnse  8083  poseq  8108  mpoxopynvov0g  8164  issmo2  8289  smores  8292  smogt  8307  rdglim2  8371  tz7.48lem  8380  tz7.49  8384  swoer  8675  qsss  8722  domtriord  9061  findcard  9098  findcard2  9099  pssnn  9103  ssfiALT  9108  findcard3  9193  frfi  9195  dffi3  9344  supmo  9365  infmo  9410  inf3lem4  9552  frinsg  9675  carddom2  9901  fidomtri2  9918  pm54.43  9925  infpwfien  9984  alephordi  9996  cardaleph  10011  carduniima  10018  cardinfima  10019  alephval3  10032  dfac5lem4  10048  dfac5lem4OLD  10050  dfac5  10051  dfac2b  10053  kmlem2  10074  cflm  10172  cfslb2n  10190  cfsmolem  10192  isf32lem9  10283  axcc4  10361  domtriomlem  10364  zorn2lem4  10421  zorn2lem6  10423  fpwwe2lem10  10563  fpwwe2lem11  10564  inttsk  10697  inar1  10698  intgru  10737  ingru  10738  indpi  10830  nqpr  10937  ltaddpr  10957  ltexprlem1  10959  ltexprlem5  10963  reclem2pr  10971  reclem4pr  10973  negn0  11579  zmulcl  12576  uzm1  12822  uzwo  12861  xmullem2  13217  icoshft  13426  difreicc  13437  fzouzsplit  13649  ssfzoulel  13715  seqf1olem1  14003  seqf1olem2  14004  hashge2el2difr  14443  hashtpg  14447  reusq0  15427  modfsummod  15757  incexclem  15801  sqrt2irr  16216  dvds2lem  16237  dvdslelem  16278  oddnn02np1  16317  divalglem8  16369  dfgcd2  16515  2mulprm  16662  ge2nprmge4  16671  euclemma  16683  iserodd  16806  ramcl  17000  setsstruct  17146  mreiincl  17558  joinfval  18337  meetfval  18351  dirge  18569  chnccat  18592  kerf1ghm  19222  sylow2alem1  19592  efgredlemb  19721  isdomn4  20693  rmodislmodlem  20924  lbspss  21077  lspsneu  21121  lspsnat  21143  lspsncv0  21144  opsrtoslem2  22034  distop  22960  epttop  22974  isclo2  23053  restdis  23143  subbascn  23219  cnrest2  23251  cnpresti  23253  isnrm2  23323  cmpsublem  23364  cmpcld  23367  dfconn2  23384  t1connperf  23401  1stcrest  23418  lly1stc  23461  uptx  23590  txcn  23591  prdstopn  23593  txconn  23654  cmphaushmeo  23765  fbasrn  23849  csdfil  23859  trufil  23875  fclscf  23990  alexsubALTlem3  24014  alexsubALT  24016  haustsms2  24102  ovoliunlem1  25469  ovoliunnul  25474  volsup2  25572  coeaddlem  26214  plymul0or  26247  radcnv0  26381  rtprmirr  26724  wilthlem3  27033  chtub  27175  gausslemma2dlem1a  27328  2sqlem10  27391  pntpbnd1  27549  ltsval2  27620  noetalem1  27705  bday1  27806  mpteleeOLD  28964  axeuclidlem  29031  axcontlem4  29036  elntg2  29054  uhgrissubgr  29344  finsumvtxdg2size  29619  wlkonl1iedg  29732  pthdivtx  29795  pthisspthorcycl  29870  wlkiswwlksupgr2  29945  eucrct2eupth  30315  isch3  31312  shmodsi  31460  orthin  31517  h1datomi  31652  stcltr2i  32346  atom1d  32424  sumdmdii  32486  cdj3lem1  32505  disjpreima  32654  lmxrge0  34096  dmvlsiga  34273  sibfof  34484  bnj600  35061  bnj1018g  35105  bnj1018  35106  bnj1173  35144  bnj1174  35145  trssfir1om  35255  trssfir1omregs  35280  onvf1odlem2  35286  onvf1odlem4  35288  subgrwlk  35314  cusgracyclt3v  35338  erdszelem9  35381  cvmlift2lem1  35484  satfvsucsuc  35547  sat1el2xp  35561  fmla0xp  35565  3jcadALT  35869  fundmpss  35949  outsideofrflx  36309  nn0prpwlem  36504  ivthALT  36517  fnessref  36539  neibastop2lem  36542  tailfb  36559  mh-inf3f1  36723  bj-axtd  36859  bj-nfimt  36917  bj-nfdt0  36992  bj-nnfand  37052  bj-sbievw2  37153  bj-2upleq  37319  bj-restn0  37402  icorempo  37667  isbasisrelowllem2  37672  rdgellim  37692  rdgssun  37694  pibt2  37733  wl-lem-moexsb  37893  matunitlindflem1  37937  poimirlem3  37944  poimirlem4  37945  poimirlem29  37970  mblfinlem3  37980  itg2addnclem3  37994  cover2  38036  fdc  38066  nninfnub  38072  equivtotbnd  38099  prdstotbnd  38115  cntotbnd  38117  ablo4pnp  38201  isdrngo3  38280  crngohomfo  38327  intidl  38350  or32dd  38415  iss2  38665  refressn  38854  eldisjlem19  39234  prtlem18  39323  prter2  39327  lsat0cv  39479  lfl1  39516  lkreqN  39616  atlrelat1  39767  pmapsub  40214  pclclN  40337  pclfinN  40346  osumcllem4N  40405  pexmidlem1N  40416  cdleme7ga  40694  lcfl7N  41947  eu6w  43109  dflim5  43757  omabs2  43760  ss2iundf  44086  brtrclfv2  44154  ismnushort  44728  nzss  44744  3impexpbicom  44907  alrim3con13v  44960  tratrb  44963  onfrALTlem3  44971  onfrALTlem2  44973  onfrALTlem1  44975  trsspwALT2  45245  trsspwALT3  45246  relpmin  45379  relpfrlem  45380  trfr  45389  or2expropbi  47482  afv2orxorb  47676  lswn0  47904  ich2exprop  47931  prproropf1olem4  47966  paireqne  47971  reupr  47982  lighneallem4b  48072  sbgoldbwt  48253  sbgoldbst  48254  sbgoldbalt  48257  cycldlenngric  48404  isupwlkg  48613  2zrngamgm  48721  fldivexpfllog2  49041  line2ylem  49227  fdomne0  49325