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  exptOLD  178  imbi1d  343  meredith  1660  ax13b  2051  ax12v2  2213  axc15  2452  mo3  2590  mo4  2592  2mo  2674  axprlem2  5378  axprlem1OLD  5382  axprOLD  5386  axprglem  5390  frss  5607  fvn0ssdmfun  7049  tfi  7827  nneneq  9167  wemaplem2  9488  unxpwdom2  9529  cantnfp1lem3  9628  infxpenlem  9962  axpowndlem3  10550  indpi  10858  fzind  12664  injresinj  13790  seqcl2  14026  seqfveq2  14030  seqshft2  14034  monoord  14038  seqsplit  14041  seqid2  14054  seqhomo  14055  seqcoll  14470  rexuzre  15370  rexico  15371  limsupbnd2  15500  rlim2lt  15514  rlim3  15515  lo1le  15669  caurcvg  15694  lcmfunsnlem1  16661  coprmprod  16685  eulerthlem2  16807  ramtlecl  17026  sylow1lem1  19628  efgsrel  19764  elcls3  23130  cncls2  23320  cnntr  23322  filssufilg  23958  ufileu  23966  alexsubALTlem3  24096  tgpt0  24166  isucn2  24325  imasdsf1olem  24420  nmoleub2lem2  25165  ovolicc2lem3  25568  dyadmbllem  25648  dvnres  25980  rlimcnp  27017  xrlimcnp  27020  ftalem2  27125  bcmono  27328  2sqlem6  27474  mulsproplem13  28208  mulsproplem14  28209  eupth2lems  30396  mdslmd1lem1  32484  xrge0infss  32922  axpowg2  35403  axpowg3  35404  subfacp1lem6  35495  cvmliftlem7  35601  cvmliftlem10  35604  ss2mcls  35878  mclsax  35879  axtco2  36794  bj-imim11  36951  bj-sylget  37036  bj-19.21t  37196  bj-spimt2  37230  mettrifi  38216  diaintclN  41642  dibintclN  41751  dihintcl  41928  mapdh9a  42373  posbezout  42677  aks6d1c6lem3  42749  fltaccoprm  43182  fltabcoprm  43184  flt4lem5  43192  cantnfresb  43861  safesnsupfiub  43952  iunrelexp0  44238  mnuop3d  44807  imbi12VD  45408  monoordxrv  46015  natlocalincr  47412  fcoresf1  47623  rexrsb  47654  smonoord  47931  ply1mulgsumlem1  48968  setrec1lem2  50269  pgindnf  50297