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  554  dedlem0b  1044  nic-ax  1673  nic-axALT  1674  sylgt  1822  axc15  2421  2eu6  2651  reuss2  4291  ssuni  4898  omordi  8532  nnawordi  8587  nnmordi  8597  omabs  8617  omsmolem  8623  unfi  9140  alephordi  10033  dfac5  10088  dfac2a  10089  fin23lem14  10292  facdiv  14258  facwordi  14260  o1lo1  15509  rlimuni  15522  o1co  15558  rlimcn1  15560  rlimcn3  15562  rlimo1  15589  lo1add  15599  lo1mul  15600  rlimno1  15626  caucvgrlem  15645  caucvgrlem2  15647  gcdcllem1  16475  algcvgblem  16553  isprm5  16683  prmfac1  16696  infpnlem1  16887  gsummptnn0fz  19922  gsummoncoe1  22201  evls1fpws  22262  dmatscmcl  22396  decpmatmulsumfsupp  22666  pmatcollpw1lem1  22667  pmatcollpw2lem  22670  pmatcollpwfi  22675  pm2mpmhmlem1  22711  pm2mp  22718  cpmidpmatlem3  22765  cayhamlem4  22781  isclo2  22981  lmcls  23195  isnrm3  23252  dfconn2  23312  1stcrest  23346  dfac14lem  23510  cnpflf2  23893  isucn2  24172  cncfco  24806  ovolicc2lem3  25426  dyadmbllem  25506  itgcn  25752  aalioulem2  26247  aalioulem3  26248  ulmcn  26314  rlimcxp  26890  o1cxp  26891  chtppilimlem2  27391  chtppilim  27392  nosupno  27621  nosupres  27625  noinfno  27636  noinfres  27640  pthdlem1  29702  mdsymlem6  32343  crefss  33845  ss2mcls  35555  mclsax  35556  rdgprc  35777  bj-imim21  36534  bj-axtd  36577  bj-nfimt  36621  bj-nfdt  36679  bj-19.23t  36753  bj-19.36im  36754  rdgeqoa  37353  rdgssun  37361  wl-cbvmotv  37496  pclclN  39880  primrootscoprbij  42085  isnacs3  42691  syl5imp  44495  imbi12VD  44855  sbcim2gVD  44857  limsupre3lem  45723  limsupub2  45803  fcoresf1  47060  sgoldbeven3prm  47774  ply1mulgsumlem3  48367  ply1mulgsumlem4  48368