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  2454  2eu6  2684  reuss2  4274  ssuni  4896  omordi  8605  nnawordi  8661  nnmordi  8671  omabs  8691  omsmolem  8697  unfi  9217  alephordi  10183  dfac5  10237  dfac2a  10238  fin23lem14  10441  facdiv  14461  facwordi  14463  o1lo1  15736  rlimuni  15749  o1co  15785  rlimcn1  15787  rlimcn3  15789  rlimo1  15816  lo1add  15826  lo1mul  15827  rlimno1  15853  caucvgrlem  15872  caucvgrlem2  15874  gcdcllem1  16701  algcvgblem  16784  isprm5  16915  prmfac1  16928  infpnlem1  17120  gsummptnn0fz  20233  gsummoncoe1  22659  evls1fpws  22720  dmatscmcl  22851  decpmatmulsumfsupp  23124  pmatcollpw1lem1  23125  pmatcollpw2lem  23128  pmatcollpwfi  23133  pm2mpmhmlem1  23169  pm2mp  23176  cpmidpmatlem3  23223  cayhamlem4  23239  isclo2  23439  lmcls  23653  isnrm3  23710  dfconn2  23770  1stcrest  23804  dfac14lem  23969  cnpflf2  24352  isucn2  24630  cncfco  25261  ovolicc2lem3  25873  dyadmbllem  25953  itgcn  26198  aalioulem2  26693  aalioulem3  26694  ulmcn  26759  rlimcxp  27334  o1cxp  27335  chtppilimlem2  27834  chtppilim  27835  nosupno  28093  nosupres  28097  noinfno  28108  noinfres  28112  pthdlem1  30385  mdsymlem6  33043  crefss  34564  axpowg2  35928  axpowg3  35929  ss2mcls  36513  mclsax  36514  elpssmo  36649  rdgprc  36747  bj-imim21  37607  bj-axtd  37655  bj-nfimt  37713  bj-nfdt  37789  bj-19.23t  37855  rdgeqoa  38498  rdgssun  38506  wl-cbvmotv  38650  pclclN  41151  primrootscoprbij  43355  isnacs3  43925  syl5imp  45697  imbi12VD  46057  sbcim2gVD  46059  limsupre3lem  46957  limsupub2  47037  fcoresf1  48354  sgoldbeven3prm  49096  ply1mulgsumlem3  49715  ply1mulgsumlem4  49716