Theorem imbitrrdi 253

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr4g  297  nic-ax  1680  sbequ1  2260  dfmoeu  2539  2moswapv  2633  mopick2  2641  2moswap  2648  2eu6  2661  necon3d  2956  necon1d  2957  ralrimd  3245  spcimegf  3499  spcegf  3537  spcimedv  3540  spc2gv  3545  spc3gv  3549  rspcimedv  3558  2reu1  3836  pwpw0  4751  sssn  4764  ssiun  4983  ssiun2  4984  replem  5217  wefrc  5619  ssrel  5733  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  6997  dffo4  7051  dffo5  7052  tpres  7152  fvclss  7192  isomin  7288  isofrlem  7291  isoselem  7292  fnoprabg  7486  tfisg  7801  nnsuc  7831  f1oweALT  7921  releldmdifi  7994  bropopvvv  8036  bropfvvvvlem  8037  frxp  8073  poxp  8075  fnse  8080  poseq  8105  mpoxopynvov0g  8161  issmo2  8286  smores  8289  smogt  8304  rdglim2  8368  tz7.48lem  8377  tz7.49  8381  swoer  8672  qsss  8719  domtriord  9058  findcard  9095  findcard2  9096  pssnn  9100  ssfiALT  9105  findcard3  9190  frfi  9192  dffi3  9341  supmo  9362  infmo  9407  inf3lem4  9550  frinsg  9673  carddom2  9899  fidomtri2  9916  pm54.43  9923  infpwfien  9982  alephordi  9994  cardaleph  10009  carduniima  10016  cardinfima  10017  alephval3  10030  dfac5lem4  10046  dfac5lem4OLD  10048  dfac5  10049  dfac2b  10051  kmlem2  10072  cflm  10170  cfslb2n  10188  cfsmolem  10190  isf32lem9  10281  axcc4  10359  domtriomlem  10362  zorn2lem4  10419  zorn2lem6  10421  fpwwe2lem10  10561  fpwwe2lem11  10562  inttsk  10695  inar1  10696  intgru  10735  ingru  10736  indpi  10828  nqpr  10935  ltaddpr  10955  ltexprlem1  10957  ltexprlem5  10961  reclem2pr  10969  reclem4pr  10971  negn0  11577  zmulcl  12574  uzm1  12820  uzwo  12859  xmullem2  13215  icoshft  13424  difreicc  13435  fzouzsplit  13647  ssfzoulel  13713  seqf1olem1  14001  seqf1olem2  14002  hashge2el2difr  14441  hashtpg  14445  reusq0  15425  modfsummod  15755  incexclem  15799  sqrt2irr  16214  dvds2lem  16235  dvdslelem  16276  oddnn02np1  16315  divalglem8  16367  dfgcd2  16513  2mulprm  16660  ge2nprmge4  16669  euclemma  16681  iserodd  16804  ramcl  16998  setsstruct  17144  mreiincl  17556  joinfval  18335  meetfval  18349  dirge  18567  chnccat  18590  kerf1ghm  19220  sylow2alem1  19590  efgredlemb  19719  isdomn4  20695  rmodislmodlem  20926  lbspss  21079  lspsneu  21123  lspsnat  21145  lspsncv0  21146  opsrtoslem2  22039  distop  22985  epttop  22999  isclo2  23078  restdis  23168  subbascn  23244  cnrest2  23276  cnpresti  23278  isnrm2  23348  cmpsublem  23389  cmpcld  23392  dfconn2  23409  t1connperf  23426  1stcrest  23443  lly1stc  23486  uptx  23615  txcn  23616  prdstopn  23618  txconn  23679  cmphaushmeo  23790  fbasrn  23874  csdfil  23884  trufil  23900  fclscf  24015  alexsubALTlem3  24039  alexsubALT  24041  haustsms2  24127  ovoliunlem1  25494  ovoliunnul  25499  volsup2  25597  coeaddlem  26239  plymul0or  26272  radcnv0  26406  rtprmirr  26749  wilthlem3  27058  chtub  27200  gausslemma2dlem1a  27353  2sqlem10  27416  pntpbnd1  27574  ltsval2  27645  noetalem1  27730  bday1  27831  mpteleeOLD  28989  axeuclidlem  29056  axcontlem4  29061  elntg2  29079  uhgrissubgr  29369  finsumvtxdg2size  29644  wlkonl1iedg  29757  pthdivtx  29820  pthisspthorcycl  29895  wlkiswwlksupgr2  29970  eucrct2eupth  30340  isch3  31337  shmodsi  31485  orthin  31542  h1datomi  31677  stcltr2i  32371  atom1d  32449  sumdmdii  32511  cdj3lem1  32530  disjpreima  32680  lmxrge0  34143  dmvlsiga  34320  sibfof  34531  bnj600  35108  bnj1018g  35152  bnj1018  35153  bnj1173  35191  bnj1174  35192  trssfir1om  35299  trssfir1omregs  35324  onvf1odlem2  35339  onvf1odlem4  35341  subgrwlk  35367  cusgracyclt3v  35391  erdszelem9  35434  cvmlift2lem1  35537  satfvsucsuc  35600  sat1el2xp  35614  fmla0xp  35618  3jcadALT  35922  fundmpss  36002  outsideofrflx  36362  nn0prpwlem  36557  ivthALT  36570  fnessref  36592  neibastop2lem  36595  tailfb  36612  mh-inf3f1  36776  bj-axtd  36912  bj-nfimt  36970  bj-nfdt0  37045  bj-nnfand  37105  bj-sbievw2  37206  bj-2upleq  37372  bj-restn0  37455  icorempo  37720  isbasisrelowllem2  37725  rdgellim  37745  rdgssun  37747  pibt2  37786  wl-lem-moexsb  37946  matunitlindflem1  37990  poimirlem3  37997  poimirlem4  37998  poimirlem29  38023  mblfinlem3  38033  itg2addnclem3  38047  cover2  38089  fdc  38119  nninfnub  38125  equivtotbnd  38152  prdstotbnd  38168  cntotbnd  38170  ablo4pnp  38254  isdrngo3  38333  crngohomfo  38380  intidl  38403  or32dd  38468  iss2  38718  refressn  38907  eldisjlem19  39287  prtlem18  39376  prter2  39380  lsat0cv  39532  lfl1  39569  lkreqN  39669  atlrelat1  39820  pmapsub  40267  pclclN  40390  pclfinN  40399  osumcllem4N  40458  pexmidlem1N  40469  cdleme7ga  40747  lcfl7N  42000  eu6w  43133  dflim5  43781  omabs2  43784  ss2iundf  44110  brtrclfv2  44178  ismnushort  44752  nzss  44768  3impexpbicom  44931  alrim3con13v  44984  tratrb  44987  onfrALTlem3  44995  onfrALTlem2  44997  onfrALTlem1  44999  trsspwALT2  45269  trsspwALT3  45270  relpmin  45403  relpfrlem  45404  trfr  45413  or2expropbi  47504  afv2orxorb  47698  lswn0  47926  ich2exprop  47953  prproropf1olem4  47988  paireqne  47993  reupr  48004  lighneallem4b  48094  sbgoldbwt  48275  sbgoldbst  48276  sbgoldbalt  48279  cycldlenngric  48426  isupwlkg  48635  2zrngamgm  48743  fldivexpfllog2  49063  line2ylem  49249  fdomne0  49347