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 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1  84  exptOLD  179  imbi1d  344  meredith  1674  ax13b  2065  ax12v2  2217  axc15  2453  mo3  2591  mo4  2593  2mo  2675  axprlem2  5393  axprlem1OLD  5397  axprOLD  5401  axprglem  5405  frss  5623  fvn0ssdmfun  7071  tfi  7853  nneneq  9204  wemaplem2  9523  unxpwdom2  9564  cantnfp1lem3  9663  infxpenlem  10020  axpowndlem3  10612  indpi  10920  fzind  12723  injresinj  13851  seqcl2  14088  seqfveq2  14092  seqshft2  14096  monoord  14100  seqsplit  14103  seqid2  14116  seqhomo  14117  seqcoll  14533  rexuzre  15444  rexico  15445  limsupbnd2  15574  rlim2lt  15588  rlim3  15589  lo1le  15743  caurcvg  15768  lcmfunsnlem1  16733  coprmprod  16757  eulerthlem2  16879  ramtlecl  17098  sylow1lem1  19731  efgsrel  19867  elcls3  23314  cncls2  23504  cnntr  23506  filssufilg  24143  ufileu  24151  alexsubALTlem3  24281  tgpt0  24351  isucn2  24510  imasdsf1olem  24605  nmoleub2lem2  25350  ovolicc2lem3  25753  dyadmbllem  25833  dvnres  26165  rlimcnp  27210  xrlimcnp  27213  ftalem2  27318  bcmono  27521  2sqlem6  27667  mulsproplem13  28401  mulsproplem14  28402  eupth2lems  30726  mdslmd1lem1  32814  xrge0infss  33239  axpowg2  35681  axpowg3  35682  subfacp1lem6  35772  cvmliftlem7  35878  cvmliftlem10  35881  ss2mcls  36155  mclsax  36156  axtco2  37101  bj-imim11  37257  bj-sylget  37342  bj-19.21t  37502  bj-spimt2  37536  findcard4  38471  mettrifi  38515  diaintclN  41939  dibintclN  42048  dihintcl  42225  mapdh9a  42670  posbezout  42974  aks6d1c6lem3  43046  fltaccoprm  43494  fltabcoprm  43496  flt4lem5  43504  cantnfresb  44173  safesnsupfiub  44264  iunrelexp0  44550  mnuop3d  45103  imbi12VD  45703  monoordxrv  46317  fcoresf1  47965  rexrsb  47996  smonoord  48273  ply1mulgsumlem1  49324  setrec1lem2  50622  pgindnf  50650