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  2420  2eu6  2650  reuss2  4289  ssuni  4896  omordi  8530  nnawordi  8585  nnmordi  8595  omabs  8615  omsmolem  8621  unfi  9135  alephordi  10027  dfac5  10082  dfac2a  10083  fin23lem14  10286  facdiv  14252  facwordi  14254  o1lo1  15503  rlimuni  15516  o1co  15552  rlimcn1  15554  rlimcn3  15556  rlimo1  15583  lo1add  15593  lo1mul  15594  rlimno1  15620  caucvgrlem  15639  caucvgrlem2  15641  gcdcllem1  16469  algcvgblem  16547  isprm5  16677  prmfac1  16690  infpnlem1  16881  gsummptnn0fz  19916  gsummoncoe1  22195  evls1fpws  22256  dmatscmcl  22390  decpmatmulsumfsupp  22660  pmatcollpw1lem1  22661  pmatcollpw2lem  22664  pmatcollpwfi  22669  pm2mpmhmlem1  22705  pm2mp  22712  cpmidpmatlem3  22759  cayhamlem4  22775  isclo2  22975  lmcls  23189  isnrm3  23246  dfconn2  23306  1stcrest  23340  dfac14lem  23504  cnpflf2  23887  isucn2  24166  cncfco  24800  ovolicc2lem3  25420  dyadmbllem  25500  itgcn  25746  aalioulem2  26241  aalioulem3  26242  ulmcn  26308  rlimcxp  26884  o1cxp  26885  chtppilimlem2  27385  chtppilim  27386  nosupno  27615  nosupres  27619  noinfno  27630  noinfres  27634  pthdlem1  29696  mdsymlem6  32337  crefss  33839  ss2mcls  35555  mclsax  35556  rdgprc  35782  bj-imim21  36539  bj-axtd  36582  bj-nfimt  36626  bj-nfdt  36684  bj-19.23t  36758  bj-19.36im  36759  rdgeqoa  37358  rdgssun  37366  wl-cbvmotv  37501  pclclN  39885  primrootscoprbij  42090  isnacs3  42698  syl5imp  44502  imbi12VD  44862  sbcim2gVD  44864  limsupre3lem  45730  limsupub2  45810  fcoresf1  47070  sgoldbeven3prm  47784  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378