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  330  meredith  1606  nfimt  1861  ax13b  2006  ax12v2  2089  sbequi  2403  mo3  2536  2mo  2580  sstr2  3643  ssralv  3699  soss  5082  frss  5110  fvn0ssdmfun  6390  tfi  7095  nneneq  8184  wemaplem2  8493  unxpwdom2  8534  cantnfp1lem3  8615  infxpenlem  8874  axpowndlem3  9459  indpi  9767  fzind  11513  injresinj  12629  seqcl2  12859  seqfveq2  12863  seqshft2  12867  monoord  12871  seqsplit  12874  seqid2  12887  seqhomo  12888  seqcoll  13286  rexuzre  14136  rexico  14137  limsupbnd2  14258  rlim2lt  14272  rlim3  14273  lo1le  14426  caurcvg  14451  lcmfunsnlem1  15397  coprmprod  15422  eulerthlem2  15534  ramtlecl  15751  sylow1lem1  18059  efgsrel  18193  elcls3  20935  cncls2  21125  cnntr  21127  filssufilg  21762  ufileu  21770  alexsubALTlem3  21900  tgpt0  21969  isucn2  22130  imasdsf1olem  22225  nmoleub2lem2  22962  ovolicc2lem3  23333  dyadmbllem  23413  dvnres  23739  rlimcnp  24737  xrlimcnp  24740  ftalem2  24845  bcmono  25047  2sqlem6  25193  eupth2lems  27216  mdslmd1lem1  29312  xrge0infss  29653  subfacp1lem6  31293  cvmliftlem7  31399  cvmliftlem10  31402  ss2mcls  31591  mclsax  31592  bj-exlimh  32727  bj-spimt2  32834  wl-ax8clv2  33511  mettrifi  33683  diaintclN  36664  dibintclN  36773  dihintcl  36950  mapdh9a  37396  iunrelexp0  38311  imbi12VD  39423  monoordxrv  40025  smonoord  41666  ply1mulgsumlem1  42499  setrec1lem2  42760