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  1675  nic-axALT  1676  sylgt  1824  axc15  2427  2eu6  2658  reuss2  4280  ssuni  4890  omordi  8503  nnawordi  8559  nnmordi  8569  omabs  8589  omsmolem  8595  unfi  9107  alephordi  9996  dfac5  10051  dfac2a  10052  fin23lem14  10255  facdiv  14222  facwordi  14224  o1lo1  15472  rlimuni  15485  o1co  15521  rlimcn1  15523  rlimcn3  15525  rlimo1  15552  lo1add  15562  lo1mul  15563  rlimno1  15589  caucvgrlem  15608  caucvgrlem2  15610  gcdcllem1  16438  algcvgblem  16516  isprm5  16646  prmfac1  16659  infpnlem1  16850  gsummptnn0fz  19927  gsummoncoe1  22264  evls1fpws  22325  dmatscmcl  22459  decpmatmulsumfsupp  22729  pmatcollpw1lem1  22730  pmatcollpw2lem  22733  pmatcollpwfi  22738  pm2mpmhmlem1  22774  pm2mp  22781  cpmidpmatlem3  22828  cayhamlem4  22844  isclo2  23044  lmcls  23258  isnrm3  23315  dfconn2  23375  1stcrest  23409  dfac14lem  23573  cnpflf2  23956  isucn2  24234  cncfco  24868  ovolicc2lem3  25488  dyadmbllem  25568  itgcn  25814  aalioulem2  26309  aalioulem3  26310  ulmcn  26376  rlimcxp  26952  o1cxp  26953  chtppilimlem2  27453  chtppilim  27454  nosupno  27683  nosupres  27687  noinfno  27698  noinfres  27702  pthdlem1  29851  mdsymlem6  32495  crefss  34026  ss2mcls  35781  mclsax  35782  rdgprc  36005  bj-imim21  36770  bj-axtd  36815  bj-nfimt  36868  bj-nfdt  36935  bj-19.23t  36999  bj-19.36im  37000  rdgeqoa  37619  rdgssun  37627  wl-cbvmotv  37762  pclclN  40261  primrootscoprbij  42466  isnacs3  43061  syl5imp  44862  imbi12VD  45222  sbcim2gVD  45224  limsupre3lem  46084  limsupub2  46164  fcoresf1  47423  sgoldbeven3prm  48137  ply1mulgsumlem3  48742  ply1mulgsumlem4  48743