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  1641  ax13b  2031  ax12v2  2179  axc15  2427  mo3  2564  mo4  2566  2mo  2648  sstr2OLD  3991  ssralvOLD  4056  axprlem1  5423  axprlem2  5424  axprOLD  5431  frss  5649  fvn0ssdmfun  7094  tfi  7874  nneneq  9246  nneneqOLD  9258  wemaplem2  9587  unxpwdom2  9628  cantnfp1lem3  9720  infxpenlem  10053  axpowndlem3  10639  indpi  10947  fzind  12716  injresinj  13827  seqcl2  14061  seqfveq2  14065  seqshft2  14069  monoord  14073  seqsplit  14076  seqid2  14089  seqhomo  14090  seqcoll  14503  rexuzre  15391  rexico  15392  limsupbnd2  15519  rlim2lt  15533  rlim3  15534  lo1le  15688  caurcvg  15713  lcmfunsnlem1  16674  coprmprod  16698  eulerthlem2  16819  ramtlecl  17038  sylow1lem1  19616  efgsrel  19752  elcls3  23091  cncls2  23281  cnntr  23283  filssufilg  23919  ufileu  23927  alexsubALTlem3  24057  tgpt0  24127  isucn2  24288  imasdsf1olem  24383  nmoleub2lem2  25149  ovolicc2lem3  25554  dyadmbllem  25634  dvnres  25967  rlimcnp  27008  xrlimcnp  27011  ftalem2  27117  bcmono  27321  2sqlem6  27467  mulsproplem13  28154  mulsproplem14  28155  eupth2lems  30257  mdslmd1lem1  32344  xrge0infss  32764  subfacp1lem6  35190  cvmliftlem7  35296  cvmliftlem10  35299  ss2mcls  35573  mclsax  35574  bj-sylget  36622  bj-nfimt  36639  bj-19.21t  36770  bj-19.37im  36773  bj-spimt2  36786  mettrifi  37764  diaintclN  41060  dibintclN  41169  dihintcl  41346  mapdh9a  41791  posbezout  42101  aks6d1c6lem3  42173  fltaccoprm  42650  fltabcoprm  42652  flt4lem5  42660  cantnfresb  43337  safesnsupfiub  43429  iunrelexp0  43715  mnuop3d  44290  imbi12VD  44893  monoordxrv  45492  natlocalincr  46891  fcoresf1  47081  rexrsb  47112  smonoord  47358  ply1mulgsumlem1  48303  setrec1lem2  49207  pgindnf  49235