Theorem imim1d 80

Description: Deduction adding nested consequents. Deduction associated with imim1 81 and imim1i 61. (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 79	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  81  expt  167  imbi1d  330  meredith  1557  ax13b  1951  ax12v2  2036  ax12vOLD  2037  ax12vOLDOLD  2038  sbequi  2363  mo3  2495  2mo  2539  sstr2  3575  ssralv  3629  soss  4977  frss  5005  fvn0ssdmfun  6258  tfi  6945  nneneq  8028  wemaplem2  8335  unxpwdom2  8376  cantnfp1lem3  8460  infxpenlem  8719  axpowndlem3  9300  indpi  9608  fzind  11351  injresinj  12451  seqcl2  12681  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqid2  12709  seqhomo  12710  seqcoll  13105  rexuzre  13940  rexico  13941  limsupbnd2  14062  rlim2lt  14076  rlim3  14077  lo1le  14230  caurcvg  14255  lcmfunsnlem1  15188  coprmprod  15213  eulerthlem2  15325  ramtlecl  15542  sylow1lem1  17836  efgsrel  17970  elcls3  20697  cncls2  20887  cnntr  20889  filssufilg  21525  ufileu  21533  alexsubALTlem3  21663  tgpt0  21732  isucn2  21893  imasdsf1olem  21988  nmoleub2lem2  22724  ovolicc2lem3  23094  dyadmbllem  23173  dvnres  23500  rlimcnp  24492  xrlimcnp  24495  ftalem2  24600  bcmono  24802  2sqlem6  24948  eupath2  26507  mdslmd1lem1  28568  xrge0infss  28915  subfacp1lem6  30421  cvmliftlem7  30527  cvmliftlem10  30530  ss2mcls  30719  mclsax  30720  bj-exlimh  31787  bj-spimt2  31896  bj-nfimt  32025  mettrifi  32723  diaintclN  35365  dibintclN  35474  dihintcl  35651  mapdh9a  36097  iunrelexp0  37013  imbi12VD  38131  smonoord  39944  eupth2lems  41406  ply1mulgsumlem1  41968  setrec1lem2  42234