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  559  dedlem0b  1050  nic-ax  1680  nic-axALT  1681  sylgt  1829  axc15  2430  2eu6  2660  reuss2  4255  ssuni  4864  omordi  8492  nnawordi  8548  nnmordi  8558  omabs  8578  omsmolem  8584  unfi  9096  alephordi  9988  dfac5  10043  dfac2a  10044  fin23lem14  10247  facdiv  14241  facwordi  14243  o1lo1  15491  rlimuni  15504  o1co  15540  rlimcn1  15542  rlimcn3  15544  rlimo1  15571  lo1add  15581  lo1mul  15582  rlimno1  15608  caucvgrlem  15627  caucvgrlem2  15629  gcdcllem1  16460  algcvgblem  16538  isprm5  16669  prmfac1  16682  infpnlem1  16873  gsummptnn0fz  19953  gsummoncoe1  22295  evls1fpws  22356  dmatscmcl  22487  decpmatmulsumfsupp  22757  pmatcollpw1lem1  22758  pmatcollpw2lem  22761  pmatcollpwfi  22766  pm2mpmhmlem1  22802  pm2mp  22809  cpmidpmatlem3  22856  cayhamlem4  22872  isclo2  23072  lmcls  23286  isnrm3  23343  dfconn2  23403  1stcrest  23437  dfac14lem  23601  cnpflf2  23984  isucn2  24262  cncfco  24893  ovolicc2lem3  25505  dyadmbllem  25585  itgcn  25831  aalioulem2  26318  aalioulem3  26319  ulmcn  26383  rlimcxp  26956  o1cxp  26957  chtppilimlem2  27456  chtppilim  27457  nosupno  27686  nosupres  27690  noinfno  27701  noinfres  27705  pthdlem1  29853  mdsymlem6  32498  crefss  34042  axpowg2  35337  axpowg3  35338  ss2mcls  35805  mclsax  35806  rdgprc  36029  bj-imim21  36866  bj-axtd  36914  bj-nfimt  36972  bj-nfdt  37048  bj-19.23t  37114  rdgeqoa  37741  rdgssun  37749  wl-cbvmotv  37893  pclclN  40392  primrootscoprbij  42596  isnacs3  43168  syl5imp  44965  imbi12VD  45325  sbcim2gVD  45327  limsupre3lem  46183  limsupub2  46263  fcoresf1  47540  sgoldbeven3prm  48282  ply1mulgsumlem3  48887  ply1mulgsumlem4  48888