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  2035  ax12v2  2173  axc15  2421  mo3  2558  mo4  2560  2mo  2644  sstr2  3989  ssralv  4050  axprlem1  5421  axprlem2  5422  axpr  5426  frss  5643  fvn0ssdmfun  7076  tfi  7841  nneneq  9208  nneneqOLD  9220  wemaplem2  9541  unxpwdom2  9582  cantnfp1lem3  9674  infxpenlem  10007  axpowndlem3  10593  indpi  10901  fzind  12659  injresinj  13752  seqcl2  13985  seqfveq2  13989  seqshft2  13993  monoord  13997  seqsplit  14000  seqid2  14013  seqhomo  14014  seqcoll  14424  rexuzre  15298  rexico  15299  limsupbnd2  15426  rlim2lt  15440  rlim3  15441  lo1le  15597  caurcvg  15622  lcmfunsnlem1  16573  coprmprod  16597  eulerthlem2  16714  ramtlecl  16932  sylow1lem1  19465  efgsrel  19601  elcls3  22586  cncls2  22776  cnntr  22778  filssufilg  23414  ufileu  23422  alexsubALTlem3  23552  tgpt0  23622  isucn2  23783  imasdsf1olem  23878  nmoleub2lem2  24631  ovolicc2lem3  25035  dyadmbllem  25115  dvnres  25447  rlimcnp  26467  xrlimcnp  26470  ftalem2  26575  bcmono  26777  2sqlem6  26923  mulsproplem13  27581  mulsproplem14  27582  eupth2lems  29488  mdslmd1lem1  31573  xrge0infss  31968  subfacp1lem6  34171  cvmliftlem7  34277  cvmliftlem10  34280  ss2mcls  34554  mclsax  34555  bj-sylget  35493  bj-nfimt  35510  bj-19.21t  35642  bj-19.37im  35645  bj-spimt2  35658  mettrifi  36620  diaintclN  39924  dibintclN  40033  dihintcl  40210  mapdh9a  40655  fltaccoprm  41383  fltabcoprm  41385  flt4lem5  41393  cantnfresb  42064  safesnsupfiub  42157  iunrelexp0  42443  mnuop3d  43020  imbi12VD  43624  monoordxrv  44182  natlocalincr  45580  fcoresf1  45769  rexrsb  45798  smonoord  46029  ply1mulgsumlem1  47057  setrec1lem2  47723  pgindnf  47751