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  4267  ssuni  4876  omordi  8494  nnawordi  8550  nnmordi  8560  omabs  8580  omsmolem  8586  unfi  9098  alephordi  9987  dfac5  10042  dfac2a  10043  fin23lem14  10246  facdiv  14240  facwordi  14242  o1lo1  15490  rlimuni  15503  o1co  15539  rlimcn1  15541  rlimcn3  15543  rlimo1  15570  lo1add  15580  lo1mul  15581  rlimno1  15607  caucvgrlem  15626  caucvgrlem2  15628  gcdcllem1  16459  algcvgblem  16537  isprm5  16668  prmfac1  16681  infpnlem1  16872  gsummptnn0fz  19952  gsummoncoe1  22283  evls1fpws  22344  dmatscmcl  22478  decpmatmulsumfsupp  22748  pmatcollpw1lem1  22749  pmatcollpw2lem  22752  pmatcollpwfi  22757  pm2mpmhmlem1  22793  pm2mp  22800  cpmidpmatlem3  22847  cayhamlem4  22863  isclo2  23063  lmcls  23277  isnrm3  23334  dfconn2  23394  1stcrest  23428  dfac14lem  23592  cnpflf2  23975  isucn2  24253  cncfco  24884  ovolicc2lem3  25496  dyadmbllem  25576  itgcn  25822  aalioulem2  26310  aalioulem3  26311  ulmcn  26377  rlimcxp  26951  o1cxp  26952  chtppilimlem2  27451  chtppilim  27452  nosupno  27681  nosupres  27685  noinfno  27696  noinfres  27700  pthdlem1  29849  mdsymlem6  32494  crefss  34009  ss2mcls  35766  mclsax  35767  rdgprc  35990  bj-imim21  36827  bj-axtd  36875  bj-nfimt  36933  bj-nfdt  37009  bj-19.23t  37075  rdgeqoa  37700  rdgssun  37708  wl-cbvmotv  37852  pclclN  40351  primrootscoprbij  42555  isnacs3  43156  syl5imp  44957  imbi12VD  45317  sbcim2gVD  45319  limsupre3lem  46178  limsupub2  46258  fcoresf1  47529  sgoldbeven3prm  48271  ply1mulgsumlem3  48876  ply1mulgsumlem4  48877