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  2453  2eu6  2683  reuss2  4275  ssuni  4896  omordi  8557  nnawordi  8613  nnmordi  8623  omabs  8643  omsmolem  8649  unfi  9169  alephordi  10081  dfac5  10135  dfac2a  10136  fin23lem14  10339  facdiv  14355  facwordi  14357  o1lo1  15628  rlimuni  15641  o1co  15677  rlimcn1  15679  rlimcn3  15681  rlimo1  15708  lo1add  15718  lo1mul  15719  rlimno1  15745  caucvgrlem  15764  caucvgrlem2  15766  gcdcllem1  16595  algcvgblem  16673  isprm5  16804  prmfac1  16817  infpnlem1  17008  gsummptnn0fz  20119  gsummoncoe1  22539  evls1fpws  22600  dmatscmcl  22731  decpmatmulsumfsupp  23004  pmatcollpw1lem1  23005  pmatcollpw2lem  23008  pmatcollpwfi  23013  pm2mpmhmlem1  23049  pm2mp  23056  cpmidpmatlem3  23103  cayhamlem4  23119  isclo2  23319  lmcls  23533  isnrm3  23590  dfconn2  23650  1stcrest  23684  dfac14lem  23849  cnpflf2  24232  isucn2  24510  cncfco  25141  ovolicc2lem3  25753  dyadmbllem  25833  itgcn  26079  aalioulem2  26576  aalioulem3  26577  ulmcn  26642  rlimcxp  27218  o1cxp  27219  chtppilimlem2  27718  chtppilim  27719  nosupno  27947  nosupres  27951  noinfno  27962  noinfres  27966  pthdlem1  30239  mdsymlem6  32897  crefss  34367  axpowg2  35681  axpowg3  35682  ss2mcls  36155  mclsax  36156  rdgprc  36379  bj-imim21  37255  bj-axtd  37303  bj-nfimt  37361  bj-nfdt  37437  bj-19.23t  37503  rdgeqoa  38132  rdgssun  38140  wl-cbvmotv  38284  pclclN  40772  primrootscoprbij  42976  isnacs3  43563  syl5imp  45343  imbi12VD  45703  sbcim2gVD  45705  limsupre3lem  46568  limsupub2  46648  fcoresf1  47965  sgoldbeven3prm  48707  ply1mulgsumlem3  49326  ply1mulgsumlem4  49327