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  2426  2eu6  2656  reuss2  4301  ssuni  4908  omordi  8578  nnawordi  8633  nnmordi  8643  omabs  8663  omsmolem  8669  unfi  9185  alephordi  10088  dfac5  10143  dfac2a  10144  fin23lem14  10347  facdiv  14305  facwordi  14307  o1lo1  15553  rlimuni  15566  o1co  15602  rlimcn1  15604  rlimcn3  15606  rlimo1  15633  lo1add  15643  lo1mul  15644  rlimno1  15670  caucvgrlem  15689  caucvgrlem2  15691  gcdcllem1  16518  algcvgblem  16596  isprm5  16726  prmfac1  16739  infpnlem1  16930  gsummptnn0fz  19967  gsummoncoe1  22246  evls1fpws  22307  dmatscmcl  22441  decpmatmulsumfsupp  22711  pmatcollpw1lem1  22712  pmatcollpw2lem  22715  pmatcollpwfi  22720  pm2mpmhmlem1  22756  pm2mp  22763  cpmidpmatlem3  22810  cayhamlem4  22826  isclo2  23026  lmcls  23240  isnrm3  23297  dfconn2  23357  1stcrest  23391  dfac14lem  23555  cnpflf2  23938  isucn2  24217  cncfco  24851  ovolicc2lem3  25472  dyadmbllem  25552  itgcn  25798  aalioulem2  26293  aalioulem3  26294  ulmcn  26360  rlimcxp  26936  o1cxp  26937  chtppilimlem2  27437  chtppilim  27438  nosupno  27667  nosupres  27671  noinfno  27682  noinfres  27686  pthdlem1  29748  mdsymlem6  32389  crefss  33880  ss2mcls  35590  mclsax  35591  rdgprc  35812  bj-imim21  36569  bj-axtd  36612  bj-nfimt  36656  bj-nfdt  36714  bj-19.23t  36788  bj-19.36im  36789  rdgeqoa  37388  rdgssun  37396  wl-cbvmotv  37531  pclclN  39910  primrootscoprbij  42115  isnacs3  42733  syl5imp  44537  imbi12VD  44897  sbcim2gVD  44899  limsupre3lem  45761  limsupub2  45841  fcoresf1  47098  sgoldbeven3prm  47797  ply1mulgsumlem3  48364  ply1mulgsumlem4  48365