Theorem imim1d 83

Description: Deduction adding nested consequents. Deduction associated with imim1 84 and imim1i 64. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)

Hypothesis

Ref	Expression
imim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imim1d	⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

Proof of Theorem imim1d

Step	Hyp	Ref	Expression
1		imim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	imim12d 82	1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1  84  exptOLD  179  imbi1d  344  meredith  1674  ax13b  2065  ax12v2  2218  axc15  2457  mo3  2595  mo4  2597  2mo  2679  axprlem2  5400  axprlem1OLD  5404  axprOLD  5408  axprglem  5412  frss  5630  fvn0ssdmfun  7076  tfi  7858  nneneq  9200  wemaplem2  9519  unxpwdom2  9560  cantnfp1lem3  9659  infxpenlem  10016  axpowndlem3  10602  indpi  10910  fzind  12712  injresinj  13839  seqcl2  14076  seqfveq2  14080  seqshft2  14084  monoord  14088  seqsplit  14091  seqid2  14104  seqhomo  14105  seqcoll  14521  rexuzre  15430  rexico  15431  limsupbnd2  15560  rlim2lt  15574  rlim3  15575  lo1le  15729  caurcvg  15754  lcmfunsnlem1  16720  coprmprod  16744  eulerthlem2  16866  ramtlecl  17085  sylow1lem1  19699  efgsrel  19835  elcls3  23277  cncls2  23467  cnntr  23469  filssufilg  24105  ufileu  24113  alexsubALTlem3  24243  tgpt0  24313  isucn2  24472  imasdsf1olem  24567  nmoleub2lem2  25312  ovolicc2lem3  25715  dyadmbllem  25795  dvnres  26127  rlimcnp  27167  xrlimcnp  27170  ftalem2  27275  bcmono  27478  2sqlem6  27624  mulsproplem13  28358  mulsproplem14  28359  eupth2lems  30626  mdslmd1lem1  32714  xrge0infss  33142  axpowg2  35584  axpowg3  35585  subfacp1lem6  35698  cvmliftlem7  35804  cvmliftlem10  35807  ss2mcls  36081  mclsax  36082  axtco2  37026  bj-imim11  37182  bj-sylget  37267  bj-19.21t  37427  bj-spimt2  37461  mettrifi  38449  diaintclN  41873  dibintclN  41982  dihintcl  42159  mapdh9a  42604  posbezout  42908  aks6d1c6lem3  42980  fltaccoprm  43413  fltabcoprm  43415  flt4lem5  43423  cantnfresb  44092  safesnsupfiub  44183  iunrelexp0  44469  mnuop3d  45022  imbi12VD  45622  monoordxrv  46236  natlocalincr  47633  fcoresf1  47847  rexrsb  47878  smonoord  48155  ply1mulgsumlem1  49207  setrec1lem2  50507  pgindnf  50535