Theorem imim2d 58

Description: Deduction adding nested antecedents. Deduction associated with imim2 59 and imim2i 17. (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 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3	2	a2d 30	1 ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim2  59  embantd  60  imim12d  82  anc2r  564  dedlem0b  1060  nic-ax  1705  nic-axALT  1706  sylgt  1854  axc15  2451  2eu6  2681  reuss2  4271  ssuni  4892  omordi  8577  nnawordi  8633  nnmordi  8643  omabs  8663  omsmolem  8669  unfi  9189  alephordi  10156  dfac5  10210  dfac2a  10211  fin23lem14  10414  facdiv  14434  facwordi  14436  o1lo1  15709  rlimuni  15722  o1co  15758  rlimcn1  15760  rlimcn3  15762  rlimo1  15789  lo1add  15799  lo1mul  15800  rlimno1  15826  caucvgrlem  15845  caucvgrlem2  15847  gcdcllem1  16674  algcvgblem  16757  isprm5  16888  prmfac1  16901  infpnlem1  17093  gsummptnn0fz  20205  gsummoncoe1  22631  evls1fpws  22692  dmatscmcl  22823  decpmatmulsumfsupp  23096  pmatcollpw1lem1  23097  pmatcollpw2lem  23100  pmatcollpwfi  23105  pm2mpmhmlem1  23141  pm2mp  23148  cpmidpmatlem3  23195  cayhamlem4  23211  isclo2  23411  lmcls  23625  isnrm3  23682  dfconn2  23742  1stcrest  23776  dfac14lem  23941  cnpflf2  24324  isucn2  24602  cncfco  25233  ovolicc2lem3  25845  dyadmbllem  25925  itgcn  26170  aalioulem2  26665  aalioulem3  26666  ulmcn  26731  rlimcxp  27306  o1cxp  27307  chtppilimlem2  27806  chtppilim  27807  nosupno  28065  nosupres  28069  noinfno  28080  noinfres  28084  pthdlem1  30357  mdsymlem6  33015  crefss  34527  axpowg2  35871  axpowg3  35872  ss2mcls  36419  mclsax  36420  rdgprc  36648  bj-imim21  37508  bj-axtd  37556  bj-nfimt  37614  bj-nfdt  37690  bj-19.23t  37756  rdgeqoa  38386  rdgssun  38394  wl-cbvmotv  38538  pclclN  41041  primrootscoprbij  43245  isnacs3  43814  syl5imp  45588  imbi12VD  45948  sbcim2gVD  45950  limsupre3lem  46835  limsupub2  46915  fcoresf1  48232  sgoldbeven3prm  48974  ply1mulgsumlem3  49593  ply1mulgsumlem4  49594