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  2421  mo3  2558  mo4  2560  2mo  2642  sstr2OLD  3957  ssralvOLD  4022  axprlem1  5381  axprlem2  5382  axprOLD  5389  frss  5605  fvn0ssdmfun  7049  tfi  7832  nneneq  9176  wemaplem2  9507  unxpwdom2  9548  cantnfp1lem3  9640  infxpenlem  9973  axpowndlem3  10559  indpi  10867  fzind  12639  injresinj  13756  seqcl2  13992  seqfveq2  13996  seqshft2  14000  monoord  14004  seqsplit  14007  seqid2  14020  seqhomo  14021  seqcoll  14436  rexuzre  15326  rexico  15327  limsupbnd2  15456  rlim2lt  15470  rlim3  15471  lo1le  15625  caurcvg  15650  lcmfunsnlem1  16614  coprmprod  16638  eulerthlem2  16759  ramtlecl  16978  sylow1lem1  19535  efgsrel  19671  elcls3  22977  cncls2  23167  cnntr  23169  filssufilg  23805  ufileu  23813  alexsubALTlem3  23943  tgpt0  24013  isucn2  24173  imasdsf1olem  24268  nmoleub2lem2  25023  ovolicc2lem3  25427  dyadmbllem  25507  dvnres  25840  rlimcnp  26882  xrlimcnp  26885  ftalem2  26991  bcmono  27195  2sqlem6  27341  mulsproplem13  28038  mulsproplem14  28039  eupth2lems  30174  mdslmd1lem1  32261  xrge0infss  32690  subfacp1lem6  35179  cvmliftlem7  35285  cvmliftlem10  35288  ss2mcls  35562  mclsax  35563  bj-sylget  36616  bj-nfimt  36633  bj-19.21t  36764  bj-19.37im  36767  bj-spimt2  36780  mettrifi  37758  diaintclN  41059  dibintclN  41168  dihintcl  41345  mapdh9a  41790  posbezout  42095  aks6d1c6lem3  42167  fltaccoprm  42635  fltabcoprm  42637  flt4lem5  42645  cantnfresb  43320  safesnsupfiub  43412  iunrelexp0  43698  mnuop3d  44267  imbi12VD  44869  monoordxrv  45484  natlocalincr  46881  fcoresf1  47074  rexrsb  47105  smonoord  47376  ply1mulgsumlem1  48379  setrec1lem2  49681  pgindnf  49709