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  1706  nic-axALT  1707  sylgt  1855  axc15  2452  2eu6  2682  reuss2  4272  ssuni  4893  omordi  8558  nnawordi  8614  nnmordi  8624  omabs  8644  omsmolem  8650  unfi  9170  alephordi  10134  dfac5  10188  dfac2a  10189  fin23lem14  10392  facdiv  14411  facwordi  14413  o1lo1  15684  rlimuni  15697  o1co  15733  rlimcn1  15735  rlimcn3  15737  rlimo1  15764  lo1add  15774  lo1mul  15775  rlimno1  15801  caucvgrlem  15820  caucvgrlem2  15822  gcdcllem1  16649  algcvgblem  16732  isprm5  16863  prmfac1  16876  infpnlem1  17068  gsummptnn0fz  20180  gsummoncoe1  22606  evls1fpws  22667  dmatscmcl  22798  decpmatmulsumfsupp  23071  pmatcollpw1lem1  23072  pmatcollpw2lem  23075  pmatcollpwfi  23080  pm2mpmhmlem1  23116  pm2mp  23123  cpmidpmatlem3  23170  cayhamlem4  23186  isclo2  23386  lmcls  23600  isnrm3  23657  dfconn2  23717  1stcrest  23751  dfac14lem  23916  cnpflf2  24299  isucn2  24577  cncfco  25208  ovolicc2lem3  25820  dyadmbllem  25900  itgcn  26145  aalioulem2  26642  aalioulem3  26643  ulmcn  26708  rlimcxp  27283  o1cxp  27284  chtppilimlem2  27783  chtppilim  27784  nosupno  28042  nosupres  28046  noinfno  28057  noinfres  28061  pthdlem1  30334  mdsymlem6  32992  crefss  34463  axpowg2  35788  axpowg3  35789  ss2mcls  36302  mclsax  36303  rdgprc  36526  bj-imim21  37386  bj-axtd  37434  bj-nfimt  37492  bj-nfdt  37568  bj-19.23t  37634  rdgeqoa  38261  rdgssun  38269  wl-cbvmotv  38413  pclclN  40916  primrootscoprbij  43120  isnacs3  43674  syl5imp  45454  imbi12VD  45814  sbcim2gVD  45816  limsupre3lem  46686  limsupub2  46766  fcoresf1  48083  sgoldbeven3prm  48825  ply1mulgsumlem3  49444  ply1mulgsumlem4  49445