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  2420  mo3  2557  mo4  2559  2mo  2641  sstr2OLD  3954  ssralvOLD  4019  axprlem1  5378  axprlem2  5379  axprOLD  5386  frss  5602  fvn0ssdmfun  7046  tfi  7829  nneneq  9170  wemaplem2  9500  unxpwdom2  9541  cantnfp1lem3  9633  infxpenlem  9966  axpowndlem3  10552  indpi  10860  fzind  12632  injresinj  13749  seqcl2  13985  seqfveq2  13989  seqshft2  13993  monoord  13997  seqsplit  14000  seqid2  14013  seqhomo  14014  seqcoll  14429  rexuzre  15319  rexico  15320  limsupbnd2  15449  rlim2lt  15463  rlim3  15464  lo1le  15618  caurcvg  15643  lcmfunsnlem1  16607  coprmprod  16631  eulerthlem2  16752  ramtlecl  16971  sylow1lem1  19528  efgsrel  19664  elcls3  22970  cncls2  23160  cnntr  23162  filssufilg  23798  ufileu  23806  alexsubALTlem3  23936  tgpt0  24006  isucn2  24166  imasdsf1olem  24261  nmoleub2lem2  25016  ovolicc2lem3  25420  dyadmbllem  25500  dvnres  25833  rlimcnp  26875  xrlimcnp  26878  ftalem2  26984  bcmono  27188  2sqlem6  27334  mulsproplem13  28031  mulsproplem14  28032  eupth2lems  30167  mdslmd1lem1  32254  xrge0infss  32683  subfacp1lem6  35172  cvmliftlem7  35278  cvmliftlem10  35281  ss2mcls  35555  mclsax  35556  bj-sylget  36609  bj-nfimt  36626  bj-19.21t  36757  bj-19.37im  36760  bj-spimt2  36773  mettrifi  37751  diaintclN  41052  dibintclN  41161  dihintcl  41338  mapdh9a  41783  posbezout  42088  aks6d1c6lem3  42160  fltaccoprm  42628  fltabcoprm  42630  flt4lem5  42638  cantnfresb  43313  safesnsupfiub  43405  iunrelexp0  43691  mnuop3d  44260  imbi12VD  44862  monoordxrv  45477  natlocalincr  46874  fcoresf1  47070  rexrsb  47101  smonoord  47372  ply1mulgsumlem1  48375  setrec1lem2  49677  pgindnf  49705