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  558  dedlem0b  1040  nic-ax  1675  nic-axALT  1676  sylgt  1823  axc15  2433  2eu6  2719  reuss2  4235  ssuni  4825  omordi  8175  nnawordi  8230  nnmordi  8240  omabs  8257  omsmolem  8263  alephordi  9485  dfac5  9539  dfac2a  9540  fin23lem14  9744  facdiv  13643  facwordi  13645  o1lo1  14886  rlimuni  14899  o1co  14935  rlimcn1  14937  rlimcn2  14939  rlimo1  14965  lo1add  14975  lo1mul  14976  rlimno1  15002  caucvgrlem  15021  caucvgrlem2  15023  gcdcllem1  15838  algcvgblem  15911  isprm5  16041  prmfac1  16053  infpnlem1  16236  gsummptnn0fz  19099  gsummoncoe1  20933  dmatscmcl  21108  decpmatmulsumfsupp  21378  pmatcollpw1lem1  21379  pmatcollpw2lem  21382  pmatcollpwfi  21387  pm2mpmhmlem1  21423  pm2mp  21430  cpmidpmatlem3  21477  cayhamlem4  21493  isclo2  21693  lmcls  21907  isnrm3  21964  dfconn2  22024  1stcrest  22058  dfac14lem  22222  cnpflf2  22605  isucn2  22885  cncfco  23512  ovolicc2lem3  24123  dyadmbllem  24203  itgcn  24448  aalioulem2  24929  aalioulem3  24930  ulmcn  24994  rlimcxp  25559  o1cxp  25560  chtppilimlem2  26058  chtppilim  26059  pthdlem1  27555  mdsymlem6  30191  crefss  31202  ss2mcls  32928  mclsax  32929  rdgprc  33152  nosupno  33316  nosupres  33320  bj-imim21  33999  bj-axtd  34041  bj-nfimt  34084  bj-nfdt  34143  bj-19.23t  34214  bj-19.36im  34215  rdgeqoa  34787  rdgssun  34795  wl-cbvmotv  34918  pclclN  37187  isnacs3  39651  syl5imp  41218  imbi12VD  41579  sbcim2gVD  41581  limsupre3lem  42374  limsupub2  42454  sgoldbeven3prm  44301  ply1mulgsumlem3  44796  ply1mulgsumlem4  44797