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  1671  sbequ1  2249  dfmoeu  2539  2moswapv  2632  mopick2  2640  2moswap  2647  2eu6  2660  necon3d  2967  necon1d  2968  ralrimd  3270  spcimegf  3563  spcegf  3605  spcimedv  3608  spc2gv  3613  spc3gv  3617  rspcimedv  3626  2reu1  3919  pwpw0  4838  sssn  4851  ssiun  5069  ssiun2  5070  wefrc  5694  ssrel  5806  ssrelOLD  5807  dmcosseq  5999  dmcosseqOLD  6000  relssres  6051  trin2  6155  ssrnres  6209  sossfld  6217  reuop  6324  frpoinsg  6375  wfisgOLD  6386  tron  6418  ordtri3or  6427  oneqmini  6447  fnun  6693  f1oun  6881  brprcneu  6910  brprcneuALT  6911  ssimaex  7007  chfnrn  7082  dffo4  7137  dffo5  7138  tpres  7238  fvclss  7278  isomin  7373  isofrlem  7376  isoselem  7377  fnoprabg  7573  tfisg  7891  nnsuc  7921  f1oweALT  8013  releldmdifi  8086  bropopvvv  8131  bropfvvvvlem  8132  frxp  8167  poxp  8169  fnse  8174  poseq  8199  mpoxopynvov0g  8255  issmo2  8405  smores  8408  smogt  8423  rdglim2  8488  tz7.48lem  8497  tz7.49  8501  swoer  8794  qsss  8836  domtriord  9189  findcard  9229  findcard2  9230  pssnn  9234  ssfiALT  9241  findcard3  9346  findcard3OLD  9347  frfi  9349  dffi3  9500  supmo  9521  infmo  9564  inf3lem4  9700  frinsg  9820  carddom2  10046  fidomtri2  10063  pm54.43  10070  infpwfien  10131  alephordi  10143  cardaleph  10158  carduniima  10165  cardinfima  10166  alephval3  10179  dfac5lem4  10195  dfac5lem4OLD  10197  dfac5  10198  dfac2b  10200  kmlem2  10221  cflm  10319  cfslb2n  10337  cfsmolem  10339  isf32lem9  10430  axcc4  10508  domtriomlem  10511  zorn2lem4  10568  zorn2lem6  10570  fpwwe2lem10  10709  fpwwe2lem11  10710  inttsk  10843  inar1  10844  intgru  10883  ingru  10884  indpi  10976  nqpr  11083  ltaddpr  11103  ltexprlem1  11105  ltexprlem5  11109  reclem2pr  11117  reclem4pr  11119  negn0  11719  zmulcl  12692  uzm1  12941  uzwo  12976  xmullem2  13327  icoshft  13533  difreicc  13544  fzouzsplit  13751  ssfzoulel  13810  seqf1olem1  14092  seqf1olem2  14093  hashge2el2difr  14530  hashtpg  14534  reusq0  15511  modfsummod  15842  incexclem  15884  sqrt2irr  16297  dvds2lem  16317  dvdslelem  16357  oddnn02np1  16396  divalglem8  16448  dfgcd2  16593  2mulprm  16740  ge2nprmge4  16748  euclemma  16760  iserodd  16882  ramcl  17076  setsstruct  17223  mreiincl  17654  joinfval  18443  meetfval  18457  dirge  18673  kerf1ghm  19287  sylow2alem1  19659  efgredlemb  19788  isdomn4  20738  rmodislmodlem  20949  lbspss  21104  lspsneu  21148  lspsnat  21170  lspsncv0  21171  opsrtoslem2  22103  distop  23023  epttop  23037  isclo2  23117  restdis  23207  subbascn  23283  cnrest2  23315  cnpresti  23317  isnrm2  23387  cmpsublem  23428  cmpcld  23431  dfconn2  23448  t1connperf  23465  1stcrest  23482  lly1stc  23525  uptx  23654  txcn  23655  prdstopn  23657  txconn  23718  cmphaushmeo  23829  fbasrn  23913  csdfil  23923  trufil  23939  fclscf  24054  alexsubALTlem3  24078  alexsubALT  24080  haustsms2  24166  ovoliunlem1  25556  ovoliunnul  25561  volsup2  25659  coeaddlem  26308  plymul0or  26340  radcnv0  26477  rtprmirr  26821  wilthlem3  27131  chtub  27274  gausslemma2dlem1a  27427  2sqlem10  27490  pntpbnd1  27648  sltval2  27719  noetalem1  27804  bday1s  27894  mptelee  28928  axeuclidlem  28995  axcontlem4  29000  elntg2  29018  uhgrissubgr  29310  finsumvtxdg2size  29586  wlkonl1iedg  29701  pthdivtx  29765  wlkiswwlksupgr2  29910  eucrct2eupth  30277  isch3  31273  shmodsi  31421  orthin  31478  h1datomi  31613  stcltr2i  32307  atom1d  32385  sumdmdii  32447  cdj3lem1  32466  disjpreima  32606  lmxrge0  33898  dmvlsiga  34093  sibfof  34305  bnj600  34895  bnj1018g  34939  bnj1018  34940  bnj1173  34978  bnj1174  34979  pthisspthorcycl  35096  subgrwlk  35100  cusgracyclt3v  35124  erdszelem9  35167  cvmlift2lem1  35270  satfvsucsuc  35333  sat1el2xp  35347  fmla0xp  35351  3jcadALT  35655  fundmpss  35730  outsideofrflx  36091  nn0prpwlem  36288  ivthALT  36301  fnessref  36323  neibastop2lem  36326  tailfb  36343  bj-axtd  36560  bj-nfimt  36604  bj-nfdt0  36661  bj-nnfand  36715  bj-sbievw2  36812  bj-2upleq  36978  bj-restn0  37056  icorempo  37317  isbasisrelowllem2  37322  rdgellim  37342  rdgssun  37344  pibt2  37383  wl-lem-moexsb  37522  matunitlindflem1  37576  poimirlem3  37583  poimirlem4  37584  poimirlem29  37609  mblfinlem3  37619  itg2addnclem3  37633  cover2  37675  fdc  37705  nninfnub  37711  equivtotbnd  37738  prdstotbnd  37754  cntotbnd  37756  ablo4pnp  37840  isdrngo3  37919  crngohomfo  37966  intidl  37989  or32dd  38054  iss2  38300  refressn  38399  eldisjlem19  38766  prtlem18  38833  prter2  38837  lsat0cv  38989  lfl1  39026  lkreqN  39126  atlrelat1  39277  pmaple  39718  pmapsub  39725  pclclN  39848  pclfinN  39857  osumcllem4N  39916  pexmidlem1N  39927  cdleme7ga  40205  lcfl7N  41458  eu6w  42631  dflim5  43291  omabs2  43294  ss2iundf  43621  brtrclfv2  43689  ismnushort  44270  nzss  44286  3impexpbicom  44450  alrim3con13v  44504  tratrb  44507  onfrALTlem3  44515  onfrALTlem2  44517  onfrALTlem1  44519  trsspwALT2  44790  trsspwALT3  44791  or2expropbi  46949  afv2orxorb  47143  lswn0  47318  ich2exprop  47345  prproropf1olem4  47380  paireqne  47385  reupr  47396  lighneallem4b  47483  sbgoldbwt  47651  sbgoldbst  47652  sbgoldbalt  47655  isupwlkg  47860  2zrngamgm  47968  fldivexpfllog2  48299  line2ylem  48485  fdomne0  48563