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  341  meredith  1641  ax13b  2032  ax12v2  2180  axc15  2420  mo3  2557  mo4  2559  2mo  2641  sstr2OLD  3945  ssralvOLD  4010  axprlem1  5365  axprlem2  5366  axprOLD  5373  frss  5587  fvn0ssdmfun  7012  tfi  7793  nneneq  9130  wemaplem2  9458  unxpwdom2  9499  cantnfp1lem3  9595  infxpenlem  9926  axpowndlem3  10512  indpi  10820  fzind  12592  injresinj  13709  seqcl2  13945  seqfveq2  13949  seqshft2  13953  monoord  13957  seqsplit  13960  seqid2  13973  seqhomo  13974  seqcoll  14389  rexuzre  15278  rexico  15279  limsupbnd2  15408  rlim2lt  15422  rlim3  15423  lo1le  15577  caurcvg  15602  lcmfunsnlem1  16566  coprmprod  16590  eulerthlem2  16711  ramtlecl  16930  sylow1lem1  19495  efgsrel  19631  elcls3  22986  cncls2  23176  cnntr  23178  filssufilg  23814  ufileu  23822  alexsubALTlem3  23952  tgpt0  24022  isucn2  24182  imasdsf1olem  24277  nmoleub2lem2  25032  ovolicc2lem3  25436  dyadmbllem  25516  dvnres  25849  rlimcnp  26891  xrlimcnp  26894  ftalem2  27000  bcmono  27204  2sqlem6  27350  mulsproplem13  28054  mulsproplem14  28055  eupth2lems  30200  mdslmd1lem1  32287  xrge0infss  32716  subfacp1lem6  35160  cvmliftlem7  35266  cvmliftlem10  35269  ss2mcls  35543  mclsax  35544  bj-sylget  36597  bj-nfimt  36614  bj-19.21t  36745  bj-19.37im  36748  bj-spimt2  36761  mettrifi  37739  diaintclN  41040  dibintclN  41149  dihintcl  41326  mapdh9a  41771  posbezout  42076  aks6d1c6lem3  42148  fltaccoprm  42616  fltabcoprm  42618  flt4lem5  42626  cantnfresb  43300  safesnsupfiub  43392  iunrelexp0  43678  mnuop3d  44247  imbi12VD  44849  monoordxrv  45464  natlocalincr  46861  fcoresf1  47057  rexrsb  47088  smonoord  47359  ply1mulgsumlem1  48375  setrec1lem2  49677  pgindnf  49705