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  1044  nic-ax  1670  nic-axALT  1671  sylgt  1819  axc15  2425  2eu6  2655  reuss2  4332  ssuni  4937  omordi  8603  nnawordi  8658  nnmordi  8668  omabs  8688  omsmolem  8694  unfi  9210  alephordi  10112  dfac5  10167  dfac2a  10168  fin23lem14  10371  facdiv  14323  facwordi  14325  o1lo1  15570  rlimuni  15583  o1co  15619  rlimcn1  15621  rlimcn3  15623  rlimo1  15650  lo1add  15660  lo1mul  15661  rlimno1  15687  caucvgrlem  15706  caucvgrlem2  15708  gcdcllem1  16533  algcvgblem  16611  isprm5  16741  prmfac1  16754  infpnlem1  16944  gsummptnn0fz  20019  gsummoncoe1  22328  evls1fpws  22389  dmatscmcl  22525  decpmatmulsumfsupp  22795  pmatcollpw1lem1  22796  pmatcollpw2lem  22799  pmatcollpwfi  22804  pm2mpmhmlem1  22840  pm2mp  22847  cpmidpmatlem3  22894  cayhamlem4  22910  isclo2  23112  lmcls  23326  isnrm3  23383  dfconn2  23443  1stcrest  23477  dfac14lem  23641  cnpflf2  24024  isucn2  24304  cncfco  24947  ovolicc2lem3  25568  dyadmbllem  25648  itgcn  25895  aalioulem2  26390  aalioulem3  26391  ulmcn  26457  rlimcxp  27032  o1cxp  27033  chtppilimlem2  27533  chtppilim  27534  nosupno  27763  nosupres  27767  noinfno  27778  noinfres  27782  pthdlem1  29799  mdsymlem6  32437  crefss  33810  ss2mcls  35553  mclsax  35554  rdgprc  35776  bj-imim21  36534  bj-axtd  36577  bj-nfimt  36621  bj-nfdt  36679  bj-19.23t  36753  bj-19.36im  36754  rdgeqoa  37353  rdgssun  37361  wl-cbvmotv  37494  pclclN  39874  primrootscoprbij  42084  isnacs3  42698  syl5imp  44510  imbi12VD  44871  sbcim2gVD  44873  limsupre3lem  45688  limsupub2  45768  fcoresf1  47019  sgoldbeven3prm  47708  ply1mulgsumlem3  48234  ply1mulgsumlem4  48235