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  1674  nic-axALT  1675  sylgt  1823  axc15  2424  2eu6  2654  reuss2  4275  ssuni  4883  omordi  8487  nnawordi  8542  nnmordi  8552  omabs  8572  omsmolem  8578  unfi  9087  alephordi  9972  dfac5  10027  dfac2a  10028  fin23lem14  10231  facdiv  14196  facwordi  14198  o1lo1  15446  rlimuni  15459  o1co  15495  rlimcn1  15497  rlimcn3  15499  rlimo1  15526  lo1add  15536  lo1mul  15537  rlimno1  15563  caucvgrlem  15582  caucvgrlem2  15584  gcdcllem1  16412  algcvgblem  16490  isprm5  16620  prmfac1  16633  infpnlem1  16824  gsummptnn0fz  19900  gsummoncoe1  22224  evls1fpws  22285  dmatscmcl  22419  decpmatmulsumfsupp  22689  pmatcollpw1lem1  22690  pmatcollpw2lem  22693  pmatcollpwfi  22698  pm2mpmhmlem1  22734  pm2mp  22741  cpmidpmatlem3  22788  cayhamlem4  22804  isclo2  23004  lmcls  23218  isnrm3  23275  dfconn2  23335  1stcrest  23369  dfac14lem  23533  cnpflf2  23916  isucn2  24194  cncfco  24828  ovolicc2lem3  25448  dyadmbllem  25528  itgcn  25774  aalioulem2  26269  aalioulem3  26270  ulmcn  26336  rlimcxp  26912  o1cxp  26913  chtppilimlem2  27413  chtppilim  27414  nosupno  27643  nosupres  27647  noinfno  27658  noinfres  27662  pthdlem1  29746  mdsymlem6  32390  crefss  33883  ss2mcls  35633  mclsax  35634  rdgprc  35857  bj-imim21  36616  bj-axtd  36659  bj-nfimt  36703  bj-nfdt  36761  bj-19.23t  36835  bj-19.36im  36836  rdgeqoa  37435  rdgssun  37443  wl-cbvmotv  37578  pclclN  40010  primrootscoprbij  42215  isnacs3  42827  syl5imp  44629  imbi12VD  44989  sbcim2gVD  44991  limsupre3lem  45854  limsupub2  45934  fcoresf1  47193  sgoldbeven3prm  47907  ply1mulgsumlem3  48513  ply1mulgsumlem4  48514