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  557  dedlem0b  1039  nic-ax  1670  nic-axALT  1671  sylgt  1818  axc15  2440  sbimdvOLD  2512  sbimdOLD  2514  2eu6  2740  reuss2  4283  ssuni  4854  omordi  8186  nnawordi  8241  nnmordi  8251  omabs  8268  omsmolem  8274  alephordi  9494  dfac5  9548  dfac2a  9549  fin23lem14  9749  facdiv  13641  facwordi  13643  o1lo1  14888  rlimuni  14901  o1co  14937  rlimcn1  14939  rlimcn2  14941  rlimo1  14967  lo1add  14977  lo1mul  14978  rlimno1  15004  caucvgrlem  15023  caucvgrlem2  15025  gcdcllem1  15842  algcvgblem  15915  isprm5  16045  prmfac1  16057  infpnlem1  16240  gsummptnn0fz  19100  gsummoncoe1  20466  dmatscmcl  21106  decpmatmulsumfsupp  21375  pmatcollpw1lem1  21376  pmatcollpw2lem  21379  pmatcollpwfi  21384  pm2mpmhmlem1  21420  pm2mp  21427  cpmidpmatlem3  21474  cayhamlem4  21490  isclo2  21690  lmcls  21904  isnrm3  21961  dfconn2  22021  1stcrest  22055  dfac14lem  22219  cnpflf2  22602  isucn2  22882  cncfco  23509  ovolicc2lem3  24114  dyadmbllem  24194  itgcn  24437  aalioulem2  24916  aalioulem3  24917  ulmcn  24981  rlimcxp  25545  o1cxp  25546  chtppilimlem2  26044  chtppilim  26045  pthdlem1  27541  mdsymlem6  30179  crefss  31108  ss2mcls  32810  mclsax  32811  rdgprc  33034  nosupno  33198  nosupres  33202  bj-imim21  33881  bj-axtd  33923  bj-nfimt  33966  bj-nfdt  34025  bj-19.23t  34094  bj-19.36im  34095  rdgeqoa  34645  rdgssun  34653  wl-cbvmotv  34747  pclclN  37021  isnacs3  39300  syl5imp  40839  imbi12VD  41200  sbcim2gVD  41202  limsupre3lem  42005  limsupub2  42085  sgoldbeven3prm  43941  ply1mulgsumlem3  44435  ply1mulgsumlem4  44436