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  2536  2moswapv  2630  mopick2  2638  2moswap  2645  2eu6  2658  necon3d  2954  necon1d  2955  ralrimd  3243  spcimegf  3510  spcegf  3548  spcimedv  3551  spc2gv  3556  spc3gv  3560  rspcimedv  3569  2reu1  3849  pwpw0  4771  sssn  4784  ssiun  5004  ssiun2  5005  wefrc  5626  ssrel  5740  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  relssres  5989  trin2  6088  ssrnres  6144  sossfld  6152  reuop  6259  frpoinsg  6309  tron  6348  ordtri3or  6357  oneqmini  6378  fnun  6614  f1oun  6801  brprcneu  6832  brprcneuALT  6833  ssimaex  6927  chfnrn  7003  dffo4  7057  dffo5  7058  tpres  7157  fvclss  7197  isomin  7293  isofrlem  7296  isoselem  7297  fnoprabg  7491  tfisg  7806  nnsuc  7836  f1oweALT  7926  releldmdifi  7999  bropopvvv  8042  bropfvvvvlem  8043  frxp  8078  poxp  8080  fnse  8085  poseq  8110  mpoxopynvov0g  8166  issmo2  8291  smores  8294  smogt  8309  rdglim2  8373  tz7.48lem  8382  tz7.49  8386  swoer  8677  qsss  8724  domtriord  9063  findcard  9100  findcard2  9101  pssnn  9105  ssfiALT  9110  findcard3  9195  frfi  9197  dffi3  9346  supmo  9367  infmo  9412  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  11578  zmulcl  12552  uzm1  12797  uzwo  12836  xmullem2  13192  icoshft  13401  difreicc  13412  fzouzsplit  13622  ssfzoulel  13688  seqf1olem1  13976  seqf1olem2  13977  hashge2el2difr  14416  hashtpg  14420  reusq0  15400  modfsummod  15729  incexclem  15771  sqrt2irr  16186  dvds2lem  16207  dvdslelem  16248  oddnn02np1  16287  divalglem8  16339  dfgcd2  16485  2mulprm  16632  ge2nprmge4  16640  euclemma  16652  iserodd  16775  ramcl  16969  setsstruct  17115  mreiincl  17527  joinfval  18306  meetfval  18320  dirge  18538  chnccat  18561  kerf1ghm  19188  sylow2alem1  19558  efgredlemb  19687  isdomn4  20661  rmodislmodlem  20892  lbspss  21046  lspsneu  21090  lspsnat  21112  lspsncv0  21113  opsrtoslem2  22023  distop  22951  epttop  22965  isclo2  23044  restdis  23134  subbascn  23210  cnrest2  23242  cnpresti  23244  isnrm2  23314  cmpsublem  23355  cmpcld  23358  dfconn2  23375  t1connperf  23392  1stcrest  23409  lly1stc  23452  uptx  23581  txcn  23582  prdstopn  23584  txconn  23645  cmphaushmeo  23756  fbasrn  23840  csdfil  23850  trufil  23866  fclscf  23981  alexsubALTlem3  24005  alexsubALT  24007  haustsms2  24093  ovoliunlem1  25471  ovoliunnul  25476  volsup2  25574  coeaddlem  26222  plymul0or  26256  radcnv0  26393  rtprmirr  26738  wilthlem3  27048  chtub  27191  gausslemma2dlem1a  27344  2sqlem10  27407  pntpbnd1  27565  ltsval2  27636  noetalem1  27721  bday1  27822  mpteleeOLD  28980  axeuclidlem  29047  axcontlem4  29052  elntg2  29070  uhgrissubgr  29360  finsumvtxdg2size  29636  wlkonl1iedg  29749  pthdivtx  29812  pthisspthorcycl  29887  wlkiswwlksupgr2  29962  eucrct2eupth  30332  isch3  31328  shmodsi  31476  orthin  31533  h1datomi  31668  stcltr2i  32362  atom1d  32440  sumdmdii  32502  cdj3lem1  32521  disjpreima  32670  lmxrge0  34129  dmvlsiga  34306  sibfof  34517  bnj600  35094  bnj1018g  35138  bnj1018  35139  bnj1173  35177  bnj1174  35178  trssfir1om  35286  trssfir1omregs  35311  onvf1odlem2  35317  onvf1odlem4  35319  subgrwlk  35345  cusgracyclt3v  35369  erdszelem9  35412  cvmlift2lem1  35515  satfvsucsuc  35578  sat1el2xp  35592  fmla0xp  35596  3jcadALT  35900  fundmpss  35980  outsideofrflx  36340  nn0prpwlem  36535  ivthALT  36548  fnessref  36570  neibastop2lem  36573  tailfb  36590  bj-axtd  36815  bj-nfimt  36868  bj-nfdt0  36934  bj-nnfand  36990  bj-sbievw2  37088  bj-2upleq  37254  bj-restn0  37337  icorempo  37600  isbasisrelowllem2  37605  rdgellim  37625  rdgssun  37627  pibt2  37666  wl-lem-moexsb  37817  matunitlindflem1  37861  poimirlem3  37868  poimirlem4  37869  poimirlem29  37894  mblfinlem3  37904  itg2addnclem3  37918  cover2  37960  fdc  37990  nninfnub  37996  equivtotbnd  38023  prdstotbnd  38039  cntotbnd  38041  ablo4pnp  38125  isdrngo3  38204  crngohomfo  38251  intidl  38274  or32dd  38339  iss2  38589  refressn  38778  eldisjlem19  39158  prtlem18  39247  prter2  39251  lsat0cv  39403  lfl1  39440  lkreqN  39540  atlrelat1  39691  pmapsub  40138  pclclN  40261  pclfinN  40270  osumcllem4N  40329  pexmidlem1N  40340  cdleme7ga  40618  lcfl7N  41871  eu6w  43028  dflim5  43680  omabs2  43683  ss2iundf  44009  brtrclfv2  44077  ismnushort  44651  nzss  44667  3impexpbicom  44830  alrim3con13v  44883  tratrb  44886  onfrALTlem3  44894  onfrALTlem2  44896  onfrALTlem1  44898  trsspwALT2  45168  trsspwALT3  45169  relpmin  45302  relpfrlem  45303  trfr  45312  or2expropbi  47388  afv2orxorb  47582  lswn0  47798  ich2exprop  47825  prproropf1olem4  47860  paireqne  47865  reupr  47876  lighneallem4b  47963  sbgoldbwt  48131  sbgoldbst  48132  sbgoldbalt  48135  cycldlenngric  48282  isupwlkg  48491  2zrngamgm  48599  fldivexpfllog2  48919  line2ylem  49105  fdomne0  49203