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  2031  ax12v2  2179  axc15  2426  mo3  2563  mo4  2565  2mo  2647  sstr2OLD  3966  ssralvOLD  4031  axprlem1  5393  axprlem2  5394  axprOLD  5401  frss  5618  fvn0ssdmfun  7064  tfi  7848  nneneq  9220  wemaplem2  9561  unxpwdom2  9602  cantnfp1lem3  9694  infxpenlem  10027  axpowndlem3  10613  indpi  10921  fzind  12691  injresinj  13804  seqcl2  14038  seqfveq2  14042  seqshft2  14046  monoord  14050  seqsplit  14053  seqid2  14066  seqhomo  14067  seqcoll  14482  rexuzre  15371  rexico  15372  limsupbnd2  15499  rlim2lt  15513  rlim3  15514  lo1le  15668  caurcvg  15693  lcmfunsnlem1  16656  coprmprod  16680  eulerthlem2  16801  ramtlecl  17020  sylow1lem1  19579  efgsrel  19715  elcls3  23021  cncls2  23211  cnntr  23213  filssufilg  23849  ufileu  23857  alexsubALTlem3  23987  tgpt0  24057  isucn2  24217  imasdsf1olem  24312  nmoleub2lem2  25067  ovolicc2lem3  25472  dyadmbllem  25552  dvnres  25885  rlimcnp  26927  xrlimcnp  26930  ftalem2  27036  bcmono  27240  2sqlem6  27386  mulsproplem13  28083  mulsproplem14  28084  eupth2lems  30219  mdslmd1lem1  32306  xrge0infss  32737  subfacp1lem6  35207  cvmliftlem7  35313  cvmliftlem10  35316  ss2mcls  35590  mclsax  35591  bj-sylget  36639  bj-nfimt  36656  bj-19.21t  36787  bj-19.37im  36790  bj-spimt2  36803  mettrifi  37781  diaintclN  41077  dibintclN  41186  dihintcl  41363  mapdh9a  41808  posbezout  42113  aks6d1c6lem3  42185  fltaccoprm  42663  fltabcoprm  42665  flt4lem5  42673  cantnfresb  43348  safesnsupfiub  43440  iunrelexp0  43726  mnuop3d  44295  imbi12VD  44897  monoordxrv  45508  natlocalincr  46905  fcoresf1  47098  rexrsb  47129  smonoord  47385  ply1mulgsumlem1  48362  setrec1lem2  49552  pgindnf  49580