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  559  dedlem0b  1050  nic-ax  1680  nic-axALT  1681  sylgt  1829  axc15  2430  2eu6  2661  reuss2  4261  ssuni  4870  omordi  8498  nnawordi  8554  nnmordi  8564  omabs  8584  omsmolem  8590  unfi  9102  alephordi  9994  dfac5  10049  dfac2a  10050  fin23lem14  10253  facdiv  14247  facwordi  14249  o1lo1  15497  rlimuni  15510  o1co  15546  rlimcn1  15548  rlimcn3  15550  rlimo1  15577  lo1add  15587  lo1mul  15588  rlimno1  15614  caucvgrlem  15633  caucvgrlem2  15635  gcdcllem1  16466  algcvgblem  16544  isprm5  16675  prmfac1  16688  infpnlem1  16879  gsummptnn0fz  19959  gsummoncoe1  22301  evls1fpws  22362  dmatscmcl  22493  decpmatmulsumfsupp  22763  pmatcollpw1lem1  22764  pmatcollpw2lem  22767  pmatcollpwfi  22772  pm2mpmhmlem1  22808  pm2mp  22815  cpmidpmatlem3  22862  cayhamlem4  22878  isclo2  23078  lmcls  23292  isnrm3  23349  dfconn2  23409  1stcrest  23443  dfac14lem  23607  cnpflf2  23990  isucn2  24268  cncfco  24899  ovolicc2lem3  25511  dyadmbllem  25591  itgcn  25837  aalioulem2  26324  aalioulem3  26325  ulmcn  26389  rlimcxp  26962  o1cxp  26963  chtppilimlem2  27462  chtppilim  27463  nosupno  27692  nosupres  27696  noinfno  27707  noinfres  27711  pthdlem1  29859  mdsymlem6  32504  crefss  34040  axpowg2  35335  axpowg3  35336  ss2mcls  35803  mclsax  35804  rdgprc  36027  bj-imim21  36864  bj-axtd  36912  bj-nfimt  36970  bj-nfdt  37046  bj-19.23t  37112  rdgeqoa  37739  rdgssun  37747  wl-cbvmotv  37891  pclclN  40390  primrootscoprbij  42594  isnacs3  43166  syl5imp  44963  imbi12VD  45323  sbcim2gVD  45325  limsupre3lem  46182  limsupub2  46262  fcoresf1  47539  sgoldbeven3prm  48281  ply1mulgsumlem3  48886  ply1mulgsumlem4  48887