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  558  dedlem0b  1040  nic-ax  1675  nic-axALT  1676  sylgt  1823  axc15  2433  2eu6  2678  reuss2  4219  ssuni  4828  omordi  8207  nnawordi  8262  nnmordi  8272  omabs  8289  omsmolem  8295  unfi  8746  alephordi  9539  dfac5  9593  dfac2a  9594  fin23lem14  9798  facdiv  13702  facwordi  13704  o1lo1  14947  rlimuni  14960  o1co  14996  rlimcn1  14998  rlimcn2  15000  rlimo1  15026  lo1add  15036  lo1mul  15037  rlimno1  15063  caucvgrlem  15082  caucvgrlem2  15084  gcdcllem1  15903  algcvgblem  15978  isprm5  16108  prmfac1  16122  infpnlem1  16306  gsummptnn0fz  19179  gsummoncoe1  21033  dmatscmcl  21208  decpmatmulsumfsupp  21478  pmatcollpw1lem1  21479  pmatcollpw2lem  21482  pmatcollpwfi  21487  pm2mpmhmlem1  21523  pm2mp  21530  cpmidpmatlem3  21577  cayhamlem4  21593  isclo2  21793  lmcls  22007  isnrm3  22064  dfconn2  22124  1stcrest  22158  dfac14lem  22322  cnpflf2  22705  isucn2  22985  cncfco  23613  ovolicc2lem3  24224  dyadmbllem  24304  itgcn  24549  aalioulem2  25033  aalioulem3  25034  ulmcn  25098  rlimcxp  25663  o1cxp  25664  chtppilimlem2  26162  chtppilim  26163  pthdlem1  27659  mdsymlem6  30295  crefss  31324  ss2mcls  33050  mclsax  33051  rdgprc  33290  nosupno  33495  nosupres  33499  noinfno  33510  noinfres  33514  bj-imim21  34306  bj-axtd  34348  bj-nfimt  34391  bj-nfdt  34450  bj-19.23t  34521  bj-19.36im  34522  rdgeqoa  35093  rdgssun  35101  wl-cbvmotv  35224  pclclN  37493  isnacs3  40052  syl5imp  41619  imbi12VD  41980  sbcim2gVD  41982  limsupre3lem  42768  limsupub2  42848  sgoldbeven3prm  44696  ply1mulgsumlem3  45190  ply1mulgsumlem4  45191