Theorem imbitrrdi 254

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr4g  298  nic-ax  1692  sbequ1  2282  dfmoeu  2561  2moswapv  2655  mopick2  2663  2moswap  2670  2eu6  2682  necon3d  2977  necon1d  2978  ralrimd  3266  spcimegf  3518  spcegf  3551  spcimedv  3554  spc2gv  3559  spc3gv  3563  rspcimedv  3572  2reu1  3850  pwpw0  4770  sssn  4783  ssiun  5003  ssiun2  5004  replem  5237  wefrc  5639  ssrel  5753  dmcosseq  5952  dmcosseqOLD  5953  dmcosseqOLDOLD  5954  relssres  6006  trin2  6107  ssrnres  6160  sossfld  6168  reuop  6276  frpoinsg  6326  tron  6365  ordtri3or  6374  oneqmini  6395  fnun  6631  f1oun  6822  brprcneu  6853  brprcneuALT  6854  ssimaex  6948  chfnrn  7026  dffo4  7080  dffo5  7081  tpres  7181  fvclss  7221  isomin  7317  isofrlem  7320  isoselem  7321  fnoprabg  7515  tfisg  7830  nnsuc  7860  f1oweALT  7949  releldmdifi  8022  bropopvvv  8064  bropfvvvvlem  8065  frxp  8101  poxp  8103  fnse  8108  poseq  8133  mpoxopynvov0g  8189  issmo2  8315  smores  8318  smogt  8333  rdglim2  8398  tz7.48lem  8407  tz7.49  8411  swoer  8705  qsss  8752  domtriord  9091  findcard  9128  findcard2  9129  pssnn  9133  ssfiALT  9138  findcard3  9223  frfi  9225  dffi3  9374  supmo  9395  infmo  9440  inf3lem4  9583  frinsg  9706  carddom2  9932  fidomtri2  9949  pm54.43  9956  infpwfien  10015  alephordi  10027  cardaleph  10042  carduniima  10049  cardinfima  10050  alephval3  10063  dfac5lem4  10079  dfac5lem4OLD  10081  dfac5  10082  dfac2b  10084  kmlem2  10105  cflm  10203  cfslb2n  10222  cfsmolem  10224  isf32lem9  10315  axcc4  10393  domtriomlem  10396  zorn2lem4  10453  zorn2lem6  10455  fpwwe2lem10  10595  fpwwe2lem11  10596  inttsk  10729  inar1  10730  intgru  10769  ingru  10770  indpi  10862  nqpr  10969  ltaddpr  10989  ltexprlem1  10991  ltexprlem5  10995  reclem2pr  11003  reclem4pr  11005  negn0  11613  zmulcl  12617  uzm1  12870  uzwo  12909  xmullem2  13265  icoshft  13474  difreicc  13485  fzouzsplit  13697  ssfzoulel  13763  seqf1olem1  14051  seqf1olem2  14052  hashge2el2difr  14491  hashtpg  14495  reusq0  15475  modfsummod  15805  incexclem  15849  sqrt2irr  16264  dvds2lem  16285  dvdslelem  16326  oddnn02np1  16365  divalglem8  16417  dfgcd2  16563  2mulprm  16710  ge2nprmge4  16719  euclemma  16731  iserodd  16854  ramcl  17048  setsstruct  17195  mreiincl  17607  joinfval  18386  meetfval  18400  dirge  18618  chnccat  18641  kerf1ghm  19270  sylow2alem1  19640  efgredlemb  19769  isdomn4  20745  rmodislmodlem  20976  lbspss  21129  lspsneu  21173  lspsnat  21195  lspsncv0  21196  opsrtoslem2  22089  distop  23035  epttop  23049  isclo2  23128  restdis  23218  subbascn  23294  cnrest2  23326  cnpresti  23328  isnrm2  23398  cmpsublem  23439  cmpcld  23442  dfconn2  23459  t1connperf  23476  1stcrest  23493  lly1stc  23536  uptx  23665  txcn  23666  prdstopn  23668  txconn  23729  cmphaushmeo  23840  fbasrn  23924  csdfil  23934  trufil  23950  fclscf  24065  alexsubALTlem3  24089  alexsubALT  24091  haustsms2  24177  ovoliunlem1  25544  ovoliunnul  25549  volsup2  25647  coeaddlem  26289  plymul0or  26322  radcnv0  26456  rtprmirr  26802  wilthlem3  27111  chtub  27253  gausslemma2dlem1a  27406  2sqlem10  27469  pntpbnd1  27627  ltsval2  27697  noetalem1  27782  bday1  27884  mpteleeOLD  29042  axeuclidlem  29109  axcontlem4  29114  elntg2  29132  uhgrissubgr  29422  finsumvtxdg2size  29697  wlkonl1iedg  29810  pthdivtx  29873  pthisspthorcycl  29948  wlkiswwlksupgr2  30023  eucrct2eupth  30393  isch3  31390  shmodsi  31538  orthin  31595  h1datomi  31730  stcltr2i  32424  atom1d  32502  sumdmdii  32564  cdj3lem1  32583  disjpreima  32733  lmxrge0  34210  dmvlsiga  34387  sibfof  34598  bnj600  35178  bnj1018g  35222  bnj1018  35223  bnj1173  35261  bnj1174  35262  trssfir1om  35371  trssfir1omregs  35396  onvf1odlem2  35411  onvf1odlem4  35413  subgrwlk  35446  cusgracyclt3v  35470  erdszelem9  35513  cvmlift2lem1  35616  satfvsucsuc  35679  sat1el2xp  35693  fmla0xp  35697  3jcadALT  36001  fundmpss  36081  outsideofrflx  36441  nn0prpwlem  36646  ivthALT  36659  fnessref  36681  neibastop2lem  36684  tailfb  36701  mh-inf3f1  36865  bj-axtd  37001  bj-nfimt  37059  bj-nfdt0  37134  bj-nnfand  37194  bj-sbievw2  37295  bj-2upleq  37461  bj-restn0  37544  icorempo  37809  isbasisrelowllem2  37814  rdgellim  37834  rdgssun  37836  pibt2  37875  wl-lem-moexsb  38035  matunitlindflem1  38079  poimirlem3  38086  poimirlem4  38087  poimirlem29  38112  mblfinlem3  38122  itg2addnclem3  38136  cover2  38178  fdc  38208  nninfnub  38214  equivtotbnd  38241  prdstotbnd  38257  cntotbnd  38259  ablo4pnp  38343  isdrngo3  38422  crngohomfo  38469  intidl  38492  or32dd  38557  iss2  38807  refressn  38996  eldisjlem19  39376  prtlem18  39465  prter2  39469  lsat0cv  39621  lfl1  39658  lkreqN  39758  atlrelat1  39909  pmapsub  40356  pclclN  40479  pclfinN  40488  osumcllem4N  40547  pexmidlem1N  40558  cdleme7ga  40836  lcfl7N  42089  eu6w  43222  dflim5  43870  omabs2  43873  ss2iundf  44199  brtrclfv2  44267  ismnushort  44841  nzss  44857  3impexpbicom  45020  alrim3con13v  45073  tratrb  45076  onfrALTlem3  45084  onfrALTlem2  45086  onfrALTlem1  45088  trsspwALT2  45358  trsspwALT3  45359  relpmin  45492  relpfrlem  45493  trfr  45502  or2expropbi  47592  afv2orxorb  47786  lswn0  48014  ich2exprop  48041  prproropf1olem4  48076  paireqne  48081  reupr  48092  lighneallem4b  48182  sbgoldbwt  48363  sbgoldbst  48364  sbgoldbalt  48367  cycldlenngric  48514  isupwlkg  48723  2zrngamgm  48831  fldivexpfllog2  49151  line2ylem  49337  fdomne0  49435