Theorem imbitrrdi 251

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr4g  296  nic-ax  1676  sbequ1  2241  dfmoeu  2531  2moswapv  2626  mopick2  2634  2moswap  2641  2eu6  2653  necon3d  2962  necon1d  2963  ralrimd  3262  spcimegf  3581  spcegf  3583  spcimedv  3586  spc2gv  3591  spc3gv  3595  rspcimedv  3604  2reu1  3892  pwpw0  4817  sssn  4830  pwsnOLD  4902  ssiun  5050  ssiun2  5051  wefrc  5671  ssrel  5783  ssrelOLD  5784  dmcosseq  5973  relssres  6023  trin2  6125  ssrnres  6178  sossfld  6186  reuop  6293  frpoinsg  6345  wfisgOLD  6356  tron  6388  ordtri3or  6397  oneqmini  6417  fnun  6664  f1oun  6853  brprcneu  6882  brprcneuALT  6883  ssimaex  6977  chfnrn  7051  dffo4  7105  dffo5  7106  tpres  7202  fvclss  7241  isomin  7334  isofrlem  7337  isoselem  7338  fnoprabg  7531  tfisg  7843  nnsuc  7873  f1oweALT  7959  releldmdifi  8031  bropopvvv  8076  bropfvvvvlem  8077  frxp  8112  poxp  8114  fnse  8119  poseq  8144  mpoxopynvov0g  8199  issmo2  8349  smores  8352  smogt  8367  rdglim2  8432  tz7.48lem  8441  tz7.49  8445  swoer  8733  qsss  8772  domtriord  9123  findcard  9163  findcard2  9164  pssnn  9168  ssfiALT  9174  pssnnOLD  9265  findcard2OLD  9284  findcard3  9285  findcard3OLD  9286  frfi  9288  dffi3  9426  supmo  9447  infmo  9490  inf3lem4  9626  frinsg  9746  carddom2  9972  fidomtri2  9989  pm54.43  9996  infpwfien  10057  alephordi  10069  cardaleph  10084  carduniima  10091  cardinfima  10092  alephval3  10105  dfac5lem4  10121  dfac5  10123  dfac2b  10125  kmlem2  10146  cflm  10245  cfslb2n  10263  cfsmolem  10265  isf32lem9  10356  axcc4  10434  domtriomlem  10437  zorn2lem4  10494  zorn2lem6  10496  fpwwe2lem10  10635  fpwwe2lem11  10636  inttsk  10769  inar1  10770  intgru  10809  ingru  10810  indpi  10902  nqpr  11009  ltaddpr  11029  ltexprlem1  11031  ltexprlem5  11035  reclem2pr  11043  reclem4pr  11045  negn0  11643  zmulcl  12611  uzm1  12860  uzwo  12895  xmullem2  13244  icoshft  13450  difreicc  13461  fzouzsplit  13667  ssfzoulel  13726  seqf1olem1  14007  seqf1olem2  14008  hashge2el2difr  14442  hashtpg  14446  reusq0  15409  modfsummod  15740  incexclem  15782  sqrt2irr  16192  dvds2lem  16212  dvdslelem  16252  oddnn02np1  16291  divalglem8  16343  dfgcd2  16488  2mulprm  16630  ge2nprmge4  16638  euclemma  16650  iserodd  16768  ramcl  16962  setsstruct  17109  mreiincl  17540  joinfval  18326  meetfval  18340  dirge  18556  sylow2alem1  19485  efgredlemb  19614  kerf1ghm  20282  rmodislmodlem  20539  lbspss  20693  lspsneu  20736  lspsnat  20758  lspsncv0  20759  isdomn4  20918  opsrtoslem2  21617  distop  22498  epttop  22512  isclo2  22592  restdis  22682  subbascn  22758  cnrest2  22790  cnpresti  22792  isnrm2  22862  cmpsublem  22903  cmpcld  22906  dfconn2  22923  t1connperf  22940  1stcrest  22957  lly1stc  23000  uptx  23129  txcn  23130  prdstopn  23132  txconn  23193  cmphaushmeo  23304  fbasrn  23388  csdfil  23398  trufil  23414  fclscf  23529  alexsubALTlem3  23553  alexsubALT  23555  haustsms2  23641  ovoliunlem1  25019  ovoliunnul  25024  volsup2  25122  coeaddlem  25763  plymul0or  25794  radcnv0  25928  wilthlem3  26574  chtub  26715  gausslemma2dlem1a  26868  2sqlem10  26931  pntpbnd1  27089  sltval2  27159  noetalem1  27244  bday1s  27332  mptelee  28153  axeuclidlem  28220  axcontlem4  28225  elntg2  28243  uhgrissubgr  28532  finsumvtxdg2size  28807  wlkonl1iedg  28922  pthdivtx  28986  wlkiswwlksupgr2  29131  eucrct2eupth  29498  isch3  30494  shmodsi  30642  orthin  30699  h1datomi  30834  stcltr2i  31528  atom1d  31606  sumdmdii  31668  cdj3lem1  31687  disjpreima  31815  lmxrge0  32932  dmvlsiga  33127  sibfof  33339  bnj600  33930  bnj1018g  33974  bnj1018  33975  bnj1173  34013  bnj1174  34014  pthisspthorcycl  34119  subgrwlk  34123  cusgracyclt3v  34147  erdszelem9  34190  cvmlift2lem1  34293  satfvsucsuc  34356