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  1642  ax13b  2033  ax12v2  2184  axc15  2424  mo3  2561  mo4  2563  2mo  2645  sstr2OLD  3938  ssralvOLD  4003  axprlem1  5365  axprlem2  5366  axprOLD  5373  frss  5585  fvn0ssdmfun  7015  tfi  7791  nneneq  9124  wemaplem2  9442  unxpwdom2  9483  cantnfp1lem3  9579  infxpenlem  9913  axpowndlem3  10499  indpi  10807  fzind  12579  injresinj  13695  seqcl2  13931  seqfveq2  13935  seqshft2  13939  monoord  13943  seqsplit  13946  seqid2  13959  seqhomo  13960  seqcoll  14375  rexuzre  15264  rexico  15265  limsupbnd2  15394  rlim2lt  15408  rlim3  15409  lo1le  15563  caurcvg  15588  lcmfunsnlem1  16552  coprmprod  16576  eulerthlem2  16697  ramtlecl  16916  sylow1lem1  19514  efgsrel  19650  elcls3  23001  cncls2  23191  cnntr  23193  filssufilg  23829  ufileu  23837  alexsubALTlem3  23967  tgpt0  24037  isucn2  24196  imasdsf1olem  24291  nmoleub2lem2  25046  ovolicc2lem3  25450  dyadmbllem  25530  dvnres  25863  rlimcnp  26905  xrlimcnp  26908  ftalem2  27014  bcmono  27218  2sqlem6  27364  mulsproplem13  28070  mulsproplem14  28071  eupth2lems  30222  mdslmd1lem1  32309  xrge0infss  32749  subfacp1lem6  35252  cvmliftlem7  35358  cvmliftlem10  35361  ss2mcls  35635  mclsax  35636  bj-sylget  36688  bj-nfimt  36705  bj-19.21t  36836  bj-19.37im  36839  bj-spimt2  36852  mettrifi  37820  diaintclN  41180  dibintclN  41289  dihintcl  41466  mapdh9a  41911  posbezout  42216  aks6d1c6lem3  42288  fltaccoprm  42761  fltabcoprm  42763  flt4lem5  42771  cantnfresb  43444  safesnsupfiub  43536  iunrelexp0  43822  mnuop3d  44391  imbi12VD  44992  monoordxrv  45606  natlocalincr  47001  fcoresf1  47196  rexrsb  47227  smonoord  47498  ply1mulgsumlem1  48514  setrec1lem2  49816  pgindnf  49844