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  168  imbi1d  331  meredith  1566  nfimt  1821  ax13b  1964  ax12v2  2049  ax12vOLD  2050  ax12vOLDOLD  2051  sbequi  2375  mo3  2507  2mo  2551  sstr2  3610  ssralv  3666  soss  5053  frss  5081  fvn0ssdmfun  6350  tfi  7053  nneneq  8143  wemaplem2  8452  unxpwdom2  8493  cantnfp1lem3  8577  infxpenlem  8836  axpowndlem3  9421  indpi  9729  fzind  11475  injresinj  12589  seqcl2  12819  seqfveq2  12823  seqshft2  12827  monoord  12831  seqsplit  12834  seqid2  12847  seqhomo  12848  seqcoll  13248  rexuzre  14092  rexico  14093  limsupbnd2  14214  rlim2lt  14228  rlim3  14229  lo1le  14382  caurcvg  14407  lcmfunsnlem1  15350  coprmprod  15375  eulerthlem2  15487  ramtlecl  15704  sylow1lem1  18013  efgsrel  18147  elcls3  20887  cncls2  21077  cnntr  21079  filssufilg  21715  ufileu  21723  alexsubALTlem3  21853  tgpt0  21922  isucn2  22083  imasdsf1olem  22178  nmoleub2lem2  22916  ovolicc2lem3  23287  dyadmbllem  23367  dvnres  23694  rlimcnp  24692  xrlimcnp  24695  ftalem2  24800  bcmono  25002  2sqlem6  25148  eupth2lems  27098  mdslmd1lem1  29184  xrge0infss  29525  subfacp1lem6  31167  cvmliftlem7  31273  cvmliftlem10  31276  ss2mcls  31465  mclsax  31466  bj-exlimh  32602  bj-spimt2  32709  wl-ax8clv2  33381  mettrifi  33553  diaintclN  36347  dibintclN  36456  dihintcl  36633  mapdh9a  37079  iunrelexp0  37994  imbi12VD  39109  smonoord  41341  ply1mulgsumlem1  42174  setrec1lem2  42435