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  29023  mdsymlem6  31661  evls1fpws  32646  crefss  32829  ss2mcls  34559  mclsax  34560  rdgprc  34766  bj-imim21  35427  bj-axtd  35472  bj-nfimt  35515  bj-nfdt  35574  bj-19.23t  35648  bj-19.36im  35649  rdgeqoa  36251  rdgssun  36259  wl-cbvmotv  36382  pclclN  38762  isnacs3  41448  syl5imp  43273  imbi12VD  43634  sbcim2gVD  43636  limsupre3lem  44448  limsupub2  44528  fcoresf1  45779  sgoldbeven3prm  46451  ply1mulgsumlem3  47069  ply1mulgsumlem4  47070