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  2427  mo3  2565  mo4  2567  2mo  2649  sstr2OLD  3943  ssralvOLD  4008  axprlem1  5370  axprlem2  5371  axprOLD  5378  axprglem  5382  frss  5596  fvn0ssdmfun  7028  tfi  7805  nneneq  9142  wemaplem2  9464  unxpwdom2  9505  cantnfp1lem3  9601  infxpenlem  9935  axpowndlem3  10522  indpi  10830  fzind  12602  injresinj  13719  seqcl2  13955  seqfveq2  13959  seqshft2  13963  monoord  13967  seqsplit  13970  seqid2  13983  seqhomo  13984  seqcoll  14399  rexuzre  15288  rexico  15289  limsupbnd2  15418  rlim2lt  15432  rlim3  15433  lo1le  15587  caurcvg  15612  lcmfunsnlem1  16576  coprmprod  16600  eulerthlem2  16721  ramtlecl  16940  sylow1lem1  19539  efgsrel  19675  elcls3  23039  cncls2  23229  cnntr  23231  filssufilg  23867  ufileu  23875  alexsubALTlem3  24005  tgpt0  24075  isucn2  24234  imasdsf1olem  24329  nmoleub2lem2  25084  ovolicc2lem3  25488  dyadmbllem  25568  dvnres  25901  rlimcnp  26943  xrlimcnp  26946  ftalem2  27052  bcmono  27256  2sqlem6  27402  mulsproplem13  28136  mulsproplem14  28137  eupth2lems  30325  mdslmd1lem1  32412  xrge0infss  32850  subfacp1lem6  35398  cvmliftlem7  35504  cvmliftlem10  35507  ss2mcls  35781  mclsax  35782  bj-sylget  36853  bj-nfimt  36871  bj-19.21t  37001  bj-19.37im  37004  bj-spimt2  37030  mettrifi  38005  diaintclN  41431  dibintclN  41540  dihintcl  41717  mapdh9a  42162  posbezout  42467  aks6d1c6lem3  42539  fltaccoprm  42995  fltabcoprm  42997  flt4lem5  43005  cantnfresb  43678  safesnsupfiub  43769  iunrelexp0  44055  mnuop3d  44624  imbi12VD  45225  monoordxrv  45836  natlocalincr  47231  fcoresf1  47426  rexrsb  47457  smonoord  47728  ply1mulgsumlem1  48743  setrec1lem2  50044  pgindnf  50072