Theorem imim2d 58

Description: Deduction adding nested antecedents. Deduction associated with imim2 59 and imim2i 17. (Contributed by NM, 10-Jan-1993.)

Hypothesis

Ref	Expression
imim2d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imim2d	⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

Proof of Theorem imim2d

Step	Hyp	Ref	Expression
1		imim2d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3	2	a2d 30	1 ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim2  59  embantd  60  imim12d  82  anc2r  564  dedlem0b  1060  nic-ax  1706  nic-axALT  1707  sylgt  1855  axc15  2457  2eu6  2687  reuss2  4282  ssuni  4903  omordi  8560  nnawordi  8616  nnmordi  8626  omabs  8646  omsmolem  8652  unfi  9165  alephordi  10077  dfac5  10131  dfac2a  10132  fin23lem14  10335  facdiv  14343  facwordi  14345  o1lo1  15614  rlimuni  15627  o1co  15663  rlimcn1  15665  rlimcn3  15667  rlimo1  15694  lo1add  15704  lo1mul  15705  rlimno1  15731  caucvgrlem  15750  caucvgrlem2  15752  gcdcllem1  16582  algcvgblem  16660  isprm5  16791  prmfac1  16804  infpnlem1  16995  gsummptnn0fz  20087  gsummoncoe1  22505  evls1fpws  22566  dmatscmcl  22697  decpmatmulsumfsupp  22967  pmatcollpw1lem1  22968  pmatcollpw2lem  22971  pmatcollpwfi  22976  pm2mpmhmlem1  23012  pm2mp  23019  cpmidpmatlem3  23066  cayhamlem4  23082  isclo2  23282  lmcls  23496  isnrm3  23553  dfconn2  23613  1stcrest  23647  dfac14lem  23811  cnpflf2  24194  isucn2  24472  cncfco  25103  ovolicc2lem3  25715  dyadmbllem  25795  itgcn  26041  aalioulem2  26533  aalioulem3  26534  ulmcn  26599  rlimcxp  27175  o1cxp  27176  chtppilimlem2  27675  chtppilim  27676  nosupno  27904  nosupres  27908  noinfno  27919  noinfres  27923  pthdlem1  30152  mdsymlem6  32797  crefss  34270  axpowg2  35584  axpowg3  35585  ss2mcls  36081  mclsax  36082  rdgprc  36305  bj-imim21  37180  bj-axtd  37228  bj-nfimt  37286  bj-nfdt  37362  bj-19.23t  37428  rdgeqoa  38057  rdgssun  38065  wl-cbvmotv  38209  pclclN  40706  primrootscoprbij  42910  isnacs3  43482  syl5imp  45262  imbi12VD  45622  sbcim2gVD  45624  limsupre3lem  46487  limsupub2  46567  fcoresf1  47847  sgoldbeven3prm  48589  ply1mulgsumlem3  49209  ply1mulgsumlem4  49210