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  555  dedlem0b  1042  nic-ax  1676  nic-axALT  1677  sylgt  1824  axc15  2422  2eu6  2658  reuss2  4249  ssuni  4866  omordi  8397  nnawordi  8452  nnmordi  8462  omabs  8481  omsmolem  8487  unfi  8955  alephordi  9830  dfac5  9884  dfac2a  9885  fin23lem14  10089  facdiv  14001  facwordi  14003  o1lo1  15246  rlimuni  15259  o1co  15295  rlimcn1  15297  rlimcn3  15299  rlimo1  15326  lo1add  15336  lo1mul  15337  rlimno1  15365  caucvgrlem  15384  caucvgrlem2  15386  gcdcllem1  16206  algcvgblem  16282  isprm5  16412  prmfac1  16426  infpnlem1  16611  gsummptnn0fz  19587  gsummoncoe1  21475  dmatscmcl  21652  decpmatmulsumfsupp  21922  pmatcollpw1lem1  21923  pmatcollpw2lem  21926  pmatcollpwfi  21931  pm2mpmhmlem1  21967  pm2mp  21974  cpmidpmatlem3  22021  cayhamlem4  22037  isclo2  22239  lmcls  22453  isnrm3  22510  dfconn2  22570  1stcrest  22604  dfac14lem  22768  cnpflf2  23151  isucn2  23431  cncfco  24070  ovolicc2lem3  24683  dyadmbllem  24763  itgcn  25009  aalioulem2  25493  aalioulem3  25494  ulmcn  25558  rlimcxp  26123  o1cxp  26124  chtppilimlem2  26622  chtppilim  26623  pthdlem1  28134  mdsymlem6  30770  crefss  31799  ss2mcls  33530  mclsax  33531  rdgprc  33770  nosupno  33906  nosupres  33910  noinfno  33921  noinfres  33925  bj-imim21  34731  bj-axtd  34776  bj-nfimt  34819  bj-nfdt  34878  bj-19.23t  34952  bj-19.36im  34953  rdgeqoa  35541  rdgssun  35549  wl-cbvmotv  35672  pclclN  37905  isnacs3  40532  syl5imp  42132  imbi12VD  42493  sbcim2gVD  42495  limsupre3lem  43273  limsupub2  43353  fcoresf1  44563  sgoldbeven3prm  45235  ply1mulgsumlem3  45729  ply1mulgsumlem4  45730