Theorem imim1d 82

Description: Deduction adding nested consequents. Deduction associated with imim1 83 and imim1i 63. (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 24	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	imim12d 81	1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imim1  83  expt  177  imbi1d  342  meredith  1644  ax13b  2036  ax12v2  2174  axc15  2422  mo3  2559  mo4  2561  2mo  2645  sstr2  3990  ssralv  4051  axprlem1  5422  axprlem2  5423  axpr  5427  frss  5644  fvn0ssdmfun  7077  tfi  7842  nneneq  9209  nneneqOLD  9221  wemaplem2  9542  unxpwdom2  9583  cantnfp1lem3  9675  infxpenlem  10008  axpowndlem3  10594  indpi  10902  fzind  12660  injresinj  13753  seqcl2  13986  seqfveq2  13990  seqshft2  13994  monoord  13998  seqsplit  14001  seqid2  14014  seqhomo  14015  seqcoll  14425  rexuzre  15299  rexico  15300  limsupbnd2  15427  rlim2lt  15441  rlim3  15442  lo1le  15598  caurcvg  15623  lcmfunsnlem1  16574  coprmprod  16598  eulerthlem2  16715  ramtlecl  16933  sylow1lem1  19466  efgsrel  19602  elcls3  22587  cncls2  22777  cnntr  22779  filssufilg  23415  ufileu  23423  alexsubALTlem3  23553  tgpt0  23623  isucn2  23784  imasdsf1olem  23879  nmoleub2lem2  24632  ovolicc2lem3  25036  dyadmbllem  25116  dvnres  25448  rlimcnp  26470  xrlimcnp  26473  ftalem2  26578  bcmono  26780  2sqlem6  26926  mulsproplem13  27587  mulsproplem14  27588  eupth2lems  29522  mdslmd1lem1  31609  xrge0infss  32004  subfacp1lem6  34207  cvmliftlem7  34313  cvmliftlem10  34316  ss2mcls  34590  mclsax  34591  bj-sylget  35546  bj-nfimt  35563  bj-19.21t  35695  bj-19.37im  35698  bj-spimt2  35711  mettrifi  36673  diaintclN  39977  dibintclN  40086  dihintcl  40263  mapdh9a  40708  fltaccoprm  41430  fltabcoprm  41432  flt4lem5  41440  cantnfresb  42122  safesnsupfiub  42215  iunrelexp0  42501  mnuop3d  43078  imbi12VD  43682  monoordxrv  44240  natlocalincr  45638  fcoresf1  45827  rexrsb  45856  smonoord  46087  ply1mulgsumlem1  47115  setrec1lem2  47781  pgindnf  47809