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  2034  ax12v2  2172  axc15  2421  mo3  2563  mo4  2565  2mo  2649  sstr2  3937  ssralv  3996  axprlem1  5359  axprlem2  5360  axpr  5364  frss  5572  fvn0ssdmfun  6989  tfi  7742  nneneq  9049  nneneqOLD  9061  wemaplem2  9374  unxpwdom2  9415  cantnfp1lem3  9506  infxpenlem  9839  axpowndlem3  10425  indpi  10733  fzind  12488  injresinj  13578  seqcl2  13811  seqfveq2  13815  seqshft2  13819  monoord  13823  seqsplit  13826  seqid2  13839  seqhomo  13840  seqcoll  14247  rexuzre  15133  rexico  15134  limsupbnd2  15261  rlim2lt  15275  rlim3  15276  lo1le  15432  caurcvg  15457  lcmfunsnlem1  16409  coprmprod  16433  eulerthlem2  16550  ramtlecl  16768  sylow1lem1  19270  efgsrel  19407  elcls3  22305  cncls2  22495  cnntr  22497  filssufilg  23133  ufileu  23141  alexsubALTlem3  23271  tgpt0  23341  isucn2  23502  imasdsf1olem  23597  nmoleub2lem2  24350  ovolicc2lem3  24754  dyadmbllem  24834  dvnres  25166  rlimcnp  26186  xrlimcnp  26189  ftalem2  26294  bcmono  26496  2sqlem6  26642  eupth2lems  28710  mdslmd1lem1  30795  xrge0infss  31191  subfacp1lem6  33253  cvmliftlem7  33359  cvmliftlem10  33362  ss2mcls  33636  mclsax  33637  bj-sylget  34863  bj-nfimt  34880  bj-19.21t  35012  bj-19.37im  35015  bj-spimt2  35028  mettrifi  35975  diaintclN  39284  dibintclN  39393  dihintcl  39570  mapdh9a  40015  fltaccoprm  40687  fltabcoprm  40689  flt4lem5  40697  iunrelexp0  41538  mnuop3d  42117  imbi12VD  42721  monoordxrv  43265  fcoresf1  44822  rexrsb  44851  smonoord  45082  ply1mulgsumlem1  45986  setrec1lem2  46653  natlocalincr  46770