Theorem imim2d 57

Description: Deduction adding nested antecedents. Deduction associated with imim2 58 and imim2i 16. (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 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3	2	a2d 29	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:  imim2  58  embantd  59  imim12d  81  anc2r  554  dedlem0b  1044  nic-ax  1673  nic-axALT  1674  sylgt  1822  axc15  2420  2eu6  2650  reuss2  4279  ssuni  4886  omordi  8491  nnawordi  8546  nnmordi  8556  omabs  8576  omsmolem  8582  unfi  9095  alephordi  9987  dfac5  10042  dfac2a  10043  fin23lem14  10246  facdiv  14212  facwordi  14214  o1lo1  15462  rlimuni  15475  o1co  15511  rlimcn1  15513  rlimcn3  15515  rlimo1  15542  lo1add  15552  lo1mul  15553  rlimno1  15579  caucvgrlem  15598  caucvgrlem2  15600  gcdcllem1  16428  algcvgblem  16506  isprm5  16636  prmfac1  16649  infpnlem1  16840  gsummptnn0fz  19883  gsummoncoe1  22211  evls1fpws  22272  dmatscmcl  22406  decpmatmulsumfsupp  22676  pmatcollpw1lem1  22677  pmatcollpw2lem  22680  pmatcollpwfi  22685  pm2mpmhmlem1  22721  pm2mp  22728  cpmidpmatlem3  22775  cayhamlem4  22791  isclo2  22991  lmcls  23205  isnrm3  23262  dfconn2  23322  1stcrest  23356  dfac14lem  23520  cnpflf2  23903  isucn2  24182  cncfco  24816  ovolicc2lem3  25436  dyadmbllem  25516  itgcn  25762  aalioulem2  26257  aalioulem3  26258  ulmcn  26324  rlimcxp  26900  o1cxp  26901  chtppilimlem2  27401  chtppilim  27402  nosupno  27631  nosupres  27635  noinfno  27646  noinfres  27650  pthdlem1  29729  mdsymlem6  32370  crefss  33815  ss2mcls  35540  mclsax  35541  rdgprc  35767  bj-imim21  36524  bj-axtd  36567  bj-nfimt  36611  bj-nfdt  36669  bj-19.23t  36743  bj-19.36im  36744  rdgeqoa  37343  rdgssun  37351  wl-cbvmotv  37486  pclclN  39870  primrootscoprbij  42075  isnacs3  42683  syl5imp  44486  imbi12VD  44846  sbcim2gVD  44848  limsupre3lem  45714  limsupub2  45794  fcoresf1  47054  sgoldbeven3prm  47768  ply1mulgsumlem3  48374  ply1mulgsumlem4  48375