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  1045  nic-ax  1673  nic-axALT  1674  sylgt  1822  axc15  2427  2eu6  2657  reuss2  4326  ssuni  4932  omordi  8604  nnawordi  8659  nnmordi  8669  omabs  8689  omsmolem  8695  unfi  9211  alephordi  10114  dfac5  10169  dfac2a  10170  fin23lem14  10373  facdiv  14326  facwordi  14328  o1lo1  15573  rlimuni  15586  o1co  15622  rlimcn1  15624  rlimcn3  15626  rlimo1  15653  lo1add  15663  lo1mul  15664  rlimno1  15690  caucvgrlem  15709  caucvgrlem2  15711  gcdcllem1  16536  algcvgblem  16614  isprm5  16744  prmfac1  16757  infpnlem1  16948  gsummptnn0fz  20004  gsummoncoe1  22312  evls1fpws  22373  dmatscmcl  22509  decpmatmulsumfsupp  22779  pmatcollpw1lem1  22780  pmatcollpw2lem  22783  pmatcollpwfi  22788  pm2mpmhmlem1  22824  pm2mp  22831  cpmidpmatlem3  22878  cayhamlem4  22894  isclo2  23096  lmcls  23310  isnrm3  23367  dfconn2  23427  1stcrest  23461  dfac14lem  23625  cnpflf2  24008  isucn2  24288  cncfco  24933  ovolicc2lem3  25554  dyadmbllem  25634  itgcn  25880  aalioulem2  26375  aalioulem3  26376  ulmcn  26442  rlimcxp  27017  o1cxp  27018  chtppilimlem2  27518  chtppilim  27519  nosupno  27748  nosupres  27752  noinfno  27763  noinfres  27767  pthdlem1  29786  mdsymlem6  32427  crefss  33848  ss2mcls  35573  mclsax  35574  rdgprc  35795  bj-imim21  36552  bj-axtd  36595  bj-nfimt  36639  bj-nfdt  36697  bj-19.23t  36771  bj-19.36im  36772  rdgeqoa  37371  rdgssun  37379  wl-cbvmotv  37514  pclclN  39893  primrootscoprbij  42103  isnacs3  42721  syl5imp  44532  imbi12VD  44893  sbcim2gVD  44895  limsupre3lem  45747  limsupub2  45827  fcoresf1  47081  sgoldbeven3prm  47770  ply1mulgsumlem3  48305  ply1mulgsumlem4  48306