Theorem imim1d 83

Description: Deduction adding nested consequents. Deduction associated with imim1 84 and imim1i 64. (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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	imim12d 82	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  84  exptOLD  179  imbi1d  344  meredith  1664  ax13b  2055  ax12v2  2217  axc15  2456  mo3  2594  mo4  2596  2mo  2678  axprlem2  5385  axprlem1OLD  5389  axprOLD  5393  axprglem  5397  frss  5615  fvn0ssdmfun  7059  tfi  7837  nneneq  9178  wemaplem2  9497  unxpwdom2  9538  cantnfp1lem3  9637  infxpenlem  9985  axpowndlem3  10572  indpi  10880  fzind  12682  injresinj  13808  seqcl2  14044  seqfveq2  14048  seqshft2  14052  monoord  14056  seqsplit  14059  seqid2  14072  seqhomo  14073  seqcoll  14489  rexuzre  15392  rexico  15393  limsupbnd2  15522  rlim2lt  15536  rlim3  15537  lo1le  15691  caurcvg  15716  lcmfunsnlem1  16683  coprmprod  16707  eulerthlem2  16829  ramtlecl  17048  sylow1lem1  19656  efgsrel  19792  elcls3  23197  cncls2  23387  cnntr  23389  filssufilg  24025  ufileu  24033  alexsubALTlem3  24163  tgpt0  24233  isucn2  24392  imasdsf1olem  24487  nmoleub2lem2  25232  ovolicc2lem3  25635  dyadmbllem  25715  dvnres  26047  rlimcnp  27084  xrlimcnp  27087  ftalem2  27192  bcmono  27395  2sqlem6  27541  mulsproplem13  28275  mulsproplem14  28276  eupth2lems  30494  mdslmd1lem1  32582  xrge0infss  33013  axpowg2  35450  axpowg3  35451  subfacp1lem6  35543  cvmliftlem7  35649  cvmliftlem10  35652  ss2mcls  35926  mclsax  35927  axtco2  36842  bj-imim11  36998  bj-sylget  37083  bj-19.21t  37243  bj-spimt2  37277  mettrifi  38263  diaintclN  41689  dibintclN  41798  dihintcl  41975  mapdh9a  42420  posbezout  42724  aks6d1c6lem3  42796  fltaccoprm  43229  fltabcoprm  43231  flt4lem5  43239  cantnfresb  43908  safesnsupfiub  43999  iunrelexp0  44285  mnuop3d  44840  imbi12VD  45440  monoordxrv  46054  natlocalincr  47451  fcoresf1  47662  rexrsb  47693  smonoord  47970  ply1mulgsumlem1  49018  setrec1lem2  50318  pgindnf  50346