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  1043  nic-ax  1668  nic-axALT  1669  sylgt  1817  axc15  2416  2eu6  2647  reuss2  4311  ssuni  4930  omordi  8580  nnawordi  8635  nnmordi  8645  omabs  8665  omsmolem  8671  unfi  9188  alephordi  10089  dfac5  10143  dfac2a  10144  fin23lem14  10348  facdiv  14270  facwordi  14272  o1lo1  15505  rlimuni  15518  o1co  15554  rlimcn1  15556  rlimcn3  15558  rlimo1  15585  lo1add  15595  lo1mul  15596  rlimno1  15624  caucvgrlem  15643  caucvgrlem2  15645  gcdcllem1  16465  algcvgblem  16539  isprm5  16669  prmfac1  16683  infpnlem1  16870  gsummptnn0fz  19932  gsummoncoe1  22214  dmatscmcl  22392  decpmatmulsumfsupp  22662  pmatcollpw1lem1  22663  pmatcollpw2lem  22666  pmatcollpwfi  22671  pm2mpmhmlem1  22707  pm2mp  22714  cpmidpmatlem3  22761  cayhamlem4  22777  isclo2  22979  lmcls  23193  isnrm3  23250  dfconn2  23310  1stcrest  23344  dfac14lem  23508  cnpflf2  23891  isucn2  24171  cncfco  24814  ovolicc2lem3  25435  dyadmbllem  25515  itgcn  25761  aalioulem2  26255  aalioulem3  26256  ulmcn  26322  rlimcxp  26893  o1cxp  26894  chtppilimlem2  27394  chtppilim  27395  nosupno  27623  nosupres  27627  noinfno  27638  noinfres  27642  pthdlem1  29567  mdsymlem6  32205  evls1fpws  33182  crefss  33386  ss2mcls  35114  mclsax  35115  rdgprc  35326  bj-imim21  35962  bj-axtd  36007  bj-nfimt  36050  bj-nfdt  36109  bj-19.23t  36183  bj-19.36im  36184  rdgeqoa  36785  rdgssun  36793  wl-cbvmotv  36916  pclclN  39301  primrootscoprbij  41509  isnacs3  42052  syl5imp  43874  imbi12VD  44235  sbcim2gVD  44237  limsupre3lem  45043  limsupub2  45123  fcoresf1  46374  sgoldbeven3prm  47046  ply1mulgsumlem3  47379  ply1mulgsumlem4  47380