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  3497  spcegf  3535  spcimedv  3538  spc2gv  3543  spc3gv  3547  rspcimedv  3556  2reu1  3836  pwpw0  4757  sssn  4770  ssiun  4990  ssiun2  4991  replem  5223  wefrc  5618  ssrel  5732  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  relssres  5981  trin2  6080  ssrnres  6136  sossfld  6144  reuop  6251  frpoinsg  6301  tron  6340  ordtri3or  6349  oneqmini  6370  fnun  6606  f1oun  6793  brprcneu  6824  brprcneuALT  6825  ssimaex  6919  chfnrn  6995  dffo4  7049  dffo5  7050  tpres  7149  fvclss  7189  isomin  7285  isofrlem  7288  isoselem  7289  fnoprabg  7483  tfisg  7798  nnsuc  7828  f1oweALT  7918  releldmdifi  7991  bropopvvv  8033  bropfvvvvlem  8034  frxp  8069  poxp  8071  fnse  8076  poseq  8101  mpoxopynvov0g  8157  issmo2  8282  smores  8285  smogt  8300  rdglim2  8364  tz7.48lem  8373  tz7.49  8377  swoer  8668  qsss  8715  domtriord  9054  findcard  9091  findcard2  9092  pssnn  9096  ssfiALT  9101  findcard3  9186  frfi  9188  dffi3  9337  supmo  9358  infmo  9403  inf3lem4  9543  frinsg  9666  carddom2  9892  fidomtri2  9909  pm54.43  9916  infpwfien  9975  alephordi  9987  cardaleph  10002  carduniima  10009  cardinfima  10010  alephval3  10023  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  kmlem2  10065  cflm  10163  cfslb2n  10181  cfsmolem  10183  isf32lem9  10274  axcc4  10352  domtriomlem  10355  zorn2lem4  10412  zorn2lem6  10414  fpwwe2lem10  10554  fpwwe2lem11  10555  inttsk  10688  inar1  10689  intgru  10728  ingru  10729  indpi  10821  nqpr  10928  ltaddpr  10948  ltexprlem1  10950  ltexprlem5  10954  reclem2pr  10962  reclem4pr  10964  negn0  11570  zmulcl  12567  uzm1  12813  uzwo  12852  xmullem2  13208  icoshft  13417  difreicc  13428  fzouzsplit  13640  ssfzoulel  13706  seqf1olem1  13994  seqf1olem2  13995  hashge2el2difr  14434  hashtpg  14438  reusq0  15418  modfsummod  15748  incexclem  15792  sqrt2irr  16207  dvds2lem  16228  dvdslelem  16269  oddnn02np1  16308  divalglem8  16360  dfgcd2  16506  2mulprm  16653  ge2nprmge4  16662  euclemma  16674  iserodd  16797  ramcl  16991  setsstruct  17137  mreiincl  17549  joinfval  18328  meetfval  18342  dirge  18560  chnccat  18583  kerf1ghm  19213  sylow2alem1  19583  efgredlemb  19712  isdomn4  20684  rmodislmodlem  20915  lbspss  21069  lspsneu  21113  lspsnat  21135  lspsncv0  21136  opsrtoslem2  22044  distop  22970  epttop  22984  isclo2  23063  restdis  23153  subbascn  23229  cnrest2  23261  cnpresti  23263  isnrm2  23333  cmpsublem  23374  cmpcld  23377  dfconn2  23394  t1connperf  23411  1stcrest  23428  lly1stc  23471  uptx  23600  txcn  23601  prdstopn  23603  txconn  23664  cmphaushmeo  23775  fbasrn  23859  csdfil  23869  trufil  23885  fclscf  24000  alexsubALTlem3  24024  alexsubALT  24026  haustsms2  24112  ovoliunlem1  25479  ovoliunnul  25484  volsup2  25582  coeaddlem  26224  plymul0or  26257  radcnv0  26394  rtprmirr  26737  wilthlem3  27047  chtub  27189  gausslemma2dlem1a  27342  2sqlem10  27405  pntpbnd1  27563  ltsval2  27634  noetalem1  27719  bday1  27820  mpteleeOLD  28978  axeuclidlem  29045  axcontlem4  29050  elntg2  29068  uhgrissubgr  29358  finsumvtxdg2size  29634  wlkonl1iedg  29747  pthdivtx  29810  pthisspthorcycl  29885  wlkiswwlksupgr2  29960  eucrct2eupth  30330  isch3  31327  shmodsi  31475  orthin  31532  h1datomi  31667  stcltr2i  32361  atom1d  32439  sumdmdii  32501  cdj3lem1  32520  disjpreima  32669  lmxrge0  34112  dmvlsiga  34289  sibfof  34500  bnj600  35077  bnj1018g  35121  bnj1018  35122  bnj1173  35160  bnj1174  35161  trssfir1om  35271  trssfir1omregs  35296  onvf1odlem2  35302  onvf1odlem4  35304  subgrwlk  35330  cusgracyclt3v  35354  erdszelem9  35397  cvmlift2lem1  35500  satfvsucsuc  35563  sat1el2xp  35577  fmla0xp  35581  3jcadALT  35885  fundmpss  35965  outsideofrflx  36325  nn0prpwlem  36520  ivthALT  36533  fnessref  36555  neibastop2lem  36558  tailfb  36575  mh-inf3f1  36739  bj-axtd  36875  bj-nfimt  36933  bj-nfdt0  37008  bj-nnfand  37068  bj-sbievw2  37169  bj-2upleq  37335  bj-restn0  37418  icorempo  37681  isbasisrelowllem2  37686  rdgellim  37706  rdgssun  37708  pibt2  37747  wl-lem-moexsb  37907  matunitlindflem1  37951  poimirlem3  37958  poimirlem4  37959  poimirlem29  37984  mblfinlem3  37994  itg2addnclem3  38008  cover2  38050  fdc  38080  nninfnub  38086  equivtotbnd  38113  prdstotbnd  38129  cntotbnd  38131  ablo4pnp  38215  isdrngo3  38294  crngohomfo  38341  intidl  38364  or32dd  38429  iss2  38679  refressn  38868  eldisjlem19  39248  prtlem18  39337  prter2  39341  lsat0cv  39493  lfl1  39530  lkreqN  39630  atlrelat1  39781  pmapsub  40228  pclclN  40351  pclfinN  40360  osumcllem4N  40419  pexmidlem1N  40430  cdleme7ga  40708  lcfl7N  41961  eu6w  43123  dflim5  43775  omabs2  43778  ss2iundf  44104  brtrclfv2  44172  ismnushort  44746  nzss  44762  3impexpbicom  44925  alrim3con13v  44978  tratrb  44981  onfrALTlem3  44989  onfrALTlem2  44991  onfrALTlem1  44993  trsspwALT2  45263  trsspwALT3  45264  relpmin  45397  relpfrlem  45398  trfr  45407  or2expropbi  47494  afv2orxorb  47688  lswn0  47916  ich2exprop  47943  prproropf1olem4  47978  paireqne  47983  reupr  47994  lighneallem4b  48084  sbgoldbwt  48265  sbgoldbst  48266  sbgoldbalt  48269  cycldlenngric  48416  isupwlkg  48625  2zrngamgm  48733  fldivexpfllog2  49053  line2ylem  49239  fdomne0  49337