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  1637  ax13b  2028  ax12v2  2176  axc15  2424  mo3  2561  mo4  2563  2mo  2645  sstr2OLD  4002  ssralvOLD  4067  axprlem1  5428  axprlem2  5429  axprOLD  5436  frss  5652  fvn0ssdmfun  7093  tfi  7873  nneneq  9243  nneneqOLD  9255  wemaplem2  9584  unxpwdom2  9625  cantnfp1lem3  9717  infxpenlem  10050  axpowndlem3  10636  indpi  10944  fzind  12713  injresinj  13823  seqcl2  14057  seqfveq2  14061  seqshft2  14065  monoord  14069  seqsplit  14072  seqid2  14085  seqhomo  14086  seqcoll  14499  rexuzre  15387  rexico  15388  limsupbnd2  15515  rlim2lt  15529  rlim3  15530  lo1le  15684  caurcvg  15709  lcmfunsnlem1  16670  coprmprod  16694  eulerthlem2  16815  ramtlecl  17033  sylow1lem1  19630  efgsrel  19766  elcls3  23106  cncls2  23296  cnntr  23298  filssufilg  23934  ufileu  23942  alexsubALTlem3  24072  tgpt0  24142  isucn2  24303  imasdsf1olem  24398  nmoleub2lem2  25162  ovolicc2lem3  25567  dyadmbllem  25647  dvnres  25981  rlimcnp  27022  xrlimcnp  27025  ftalem2  27131  bcmono  27335  2sqlem6  27481  mulsproplem13  28168  mulsproplem14  28169  eupth2lems  30266  mdslmd1lem1  32353  xrge0infss  32770  subfacp1lem6  35169  cvmliftlem7  35275  cvmliftlem10  35278  ss2mcls  35552  mclsax  35553  bj-sylget  36603  bj-nfimt  36620  bj-19.21t  36751  bj-19.37im  36754  bj-spimt2  36767  mettrifi  37743  diaintclN  41040  dibintclN  41149  dihintcl  41326  mapdh9a  41771  posbezout  42081  aks6d1c6lem3  42153  fltaccoprm  42626  fltabcoprm  42628  flt4lem5  42636  cantnfresb  43313  safesnsupfiub  43405  iunrelexp0  43691  mnuop3d  44266  imbi12VD  44870  monoordxrv  45431  natlocalincr  46829  fcoresf1  47018  rexrsb  47049  smonoord  47295  ply1mulgsumlem1  48231  setrec1lem2  48918  pgindnf  48946