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  3930  ssralvOLD  3995  axprlem2  5361  axprlem1OLD  5365  axprOLD  5369  axprglem  5373  frss  5588  fvn0ssdmfun  7020  tfi  7797  nneneq  9133  wemaplem2  9455  unxpwdom2  9496  cantnfp1lem3  9592  infxpenlem  9926  axpowndlem3  10513  indpi  10821  fzind  12618  injresinj  13737  seqcl2  13973  seqfveq2  13977  seqshft2  13981  monoord  13985  seqsplit  13988  seqid2  14001  seqhomo  14002  seqcoll  14417  rexuzre  15306  rexico  15307  limsupbnd2  15436  rlim2lt  15450  rlim3  15451  lo1le  15605  caurcvg  15630  lcmfunsnlem1  16597  coprmprod  16621  eulerthlem2  16743  ramtlecl  16962  sylow1lem1  19564  efgsrel  19700  elcls3  23058  cncls2  23248  cnntr  23250  filssufilg  23886  ufileu  23894  alexsubALTlem3  24024  tgpt0  24094  isucn2  24253  imasdsf1olem  24348  nmoleub2lem2  25093  ovolicc2lem3  25496  dyadmbllem  25576  dvnres  25908  rlimcnp  26942  xrlimcnp  26945  ftalem2  27051  bcmono  27254  2sqlem6  27400  mulsproplem13  28134  mulsproplem14  28135  eupth2lems  30323  mdslmd1lem1  32411  xrge0infss  32848  subfacp1lem6  35383  cvmliftlem7  35489  cvmliftlem10  35492  ss2mcls  35766  mclsax  35767  axtco2  36672  bj-imim11  36829  bj-sylget  36914  bj-19.21t  37074  bj-spimt2  37108  mettrifi  38092  diaintclN  41518  dibintclN  41627  dihintcl  41804  mapdh9a  42249  posbezout  42553  aks6d1c6lem3  42625  fltaccoprm  43087  fltabcoprm  43089  flt4lem5  43097  cantnfresb  43770  safesnsupfiub  43861  iunrelexp0  44147  mnuop3d  44716  imbi12VD  45317  monoordxrv  45927  natlocalincr  47322  fcoresf1  47529  rexrsb  47560  smonoord  47837  ply1mulgsumlem1  48874  setrec1lem2  50175  pgindnf  50203