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  1041  nic-ax  1677  nic-axALT  1678  sylgt  1825  axc15  2422  2eu6  2658  reuss2  4246  ssuni  4863  omordi  8359  nnawordi  8414  nnmordi  8424  omabs  8441  omsmolem  8447  unfi  8917  alephordi  9761  dfac5  9815  dfac2a  9816  fin23lem14  10020  facdiv  13929  facwordi  13931  o1lo1  15174  rlimuni  15187  o1co  15223  rlimcn1  15225  rlimcn3  15227  rlimo1  15254  lo1add  15264  lo1mul  15265  rlimno1  15293  caucvgrlem  15312  caucvgrlem2  15314  gcdcllem1  16134  algcvgblem  16210  isprm5  16340  prmfac1  16354  infpnlem1  16539  gsummptnn0fz  19502  gsummoncoe1  21385  dmatscmcl  21560  decpmatmulsumfsupp  21830  pmatcollpw1lem1  21831  pmatcollpw2lem  21834  pmatcollpwfi  21839  pm2mpmhmlem1  21875  pm2mp  21882  cpmidpmatlem3  21929  cayhamlem4  21945  isclo2  22147  lmcls  22361  isnrm3  22418  dfconn2  22478  1stcrest  22512  dfac14lem  22676  cnpflf2  23059  isucn2  23339  cncfco  23976  ovolicc2lem3  24588  dyadmbllem  24668  itgcn  24914  aalioulem2  25398  aalioulem3  25399  ulmcn  25463  rlimcxp  26028  o1cxp  26029  chtppilimlem2  26527  chtppilim  26528  pthdlem1  28035  mdsymlem6  30671  crefss  31701  ss2mcls  33430  mclsax  33431  rdgprc  33676  nosupno  33833  nosupres  33837  noinfno  33848  noinfres  33852  bj-imim21  34658  bj-axtd  34703  bj-nfimt  34746  bj-nfdt  34805  bj-19.23t  34879  bj-19.36im  34880  rdgeqoa  35468  rdgssun  35476  wl-cbvmotv  35599  pclclN  37832  isnacs3  40448  syl5imp  42021  imbi12VD  42382  sbcim2gVD  42384  limsupre3lem  43163  limsupub2  43243  fcoresf1  44450  sgoldbeven3prm  45123  ply1mulgsumlem3  45617  ply1mulgsumlem4  45618