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  556  dedlem0b  1044  nic-ax  1676  nic-axALT  1677  sylgt  1825  axc15  2422  2eu6  2653  reuss2  4316  ssuni  4937  omordi  8566  nnawordi  8621  nnmordi  8631  omabs  8650  omsmolem  8656  unfi  9172  alephordi  10069  dfac5  10123  dfac2a  10124  fin23lem14  10328  facdiv  14247  facwordi  14249  o1lo1  15481  rlimuni  15494  o1co  15530  rlimcn1  15532  rlimcn3  15534  rlimo1  15561  lo1add  15571  lo1mul  15572  rlimno1  15600  caucvgrlem  15619  caucvgrlem2  15621  gcdcllem1  16440  algcvgblem  16514  isprm5  16644  prmfac1  16658  infpnlem1  16843  gsummptnn0fz  19854  gsummoncoe1  21828  dmatscmcl  22005  decpmatmulsumfsupp  22275  pmatcollpw1lem1  22276  pmatcollpw2lem  22279  pmatcollpwfi  22284  pm2mpmhmlem1  22320  pm2mp  22327  cpmidpmatlem3  22374  cayhamlem4  22390  isclo2  22592  lmcls  22806  isnrm3  22863  dfconn2  22923  1stcrest  22957  dfac14lem  23121  cnpflf2  23504  isucn2  23784  cncfco  24423  ovolicc2lem3  25036  dyadmbllem  25116  itgcn  25362  aalioulem2  25846  aalioulem3  25847  ulmcn  25911  rlimcxp  26478  o1cxp  26479  chtppilimlem2  26977  chtppilim  26978  nosupno  27206  nosupres  27210  noinfno  27221  noinfres  27225  pthdlem1  29054  mdsymlem6  31692  evls1fpws  32677  crefss  32860  ss2mcls  34590  mclsax  34591  rdgprc  34797  bj-imim21  35475  bj-axtd  35520  bj-nfimt  35563  bj-nfdt  35622  bj-19.23t  35696  bj-19.36im  35697  rdgeqoa  36299  rdgssun  36307  wl-cbvmotv  36430  pclclN  38810  isnacs3  41496  syl5imp  43321  imbi12VD  43682  sbcim2gVD  43684  limsupre3lem  44496  limsupub2  44576  fcoresf1  45827  sgoldbeven3prm  46499  ply1mulgsumlem3  47117  ply1mulgsumlem4  47118