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  1643  ax13b  2034  ax12v2  2187  axc15  2426  mo3  2564  mo4  2566  2mo  2648  sstr2OLD  3929  ssralvOLD  3994  axprlem2  5366  axprlem1OLD  5370  axprOLD  5374  axprglem  5378  frss  5595  fvn0ssdmfun  7026  tfi  7804  nneneq  9140  wemaplem2  9462  unxpwdom2  9503  cantnfp1lem3  9601  infxpenlem  9935  axpowndlem3  10522  indpi  10830  fzind  12627  injresinj  13746  seqcl2  13982  seqfveq2  13986  seqshft2  13990  monoord  13994  seqsplit  13997  seqid2  14010  seqhomo  14011  seqcoll  14426  rexuzre  15315  rexico  15316  limsupbnd2  15445  rlim2lt  15459  rlim3  15460  lo1le  15614  caurcvg  15639  lcmfunsnlem1  16606  coprmprod  16630  eulerthlem2  16752  ramtlecl  16971  sylow1lem1  19573  efgsrel  19709  elcls3  23048  cncls2  23238  cnntr  23240  filssufilg  23876  ufileu  23884  alexsubALTlem3  24014  tgpt0  24084  isucn2  24243  imasdsf1olem  24338  nmoleub2lem2  25083  ovolicc2lem3  25486  dyadmbllem  25566  dvnres  25898  rlimcnp  26929  xrlimcnp  26932  ftalem2  27037  bcmono  27240  2sqlem6  27386  mulsproplem13  28120  mulsproplem14  28121  eupth2lems  30308  mdslmd1lem1  32396  xrge0infss  32833  subfacp1lem6  35367  cvmliftlem7  35473  cvmliftlem10  35476  ss2mcls  35750  mclsax  35751  axtco2  36656  bj-imim11  36813  bj-sylget  36898  bj-19.21t  37058  bj-spimt2  37092  mettrifi  38078  diaintclN  41504  dibintclN  41613  dihintcl  41790  mapdh9a  42235  posbezout  42539  aks6d1c6lem3  42611  fltaccoprm  43073  fltabcoprm  43075  flt4lem5  43083  cantnfresb  43752  safesnsupfiub  43843  iunrelexp0  44129  mnuop3d  44698  imbi12VD  45299  monoordxrv  45909  natlocalincr  47306  fcoresf1  47517  rexrsb  47548  smonoord  47825  ply1mulgsumlem1  48862  setrec1lem2  50163  pgindnf  50191