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  1674  nic-axALT  1675  sylgt  1822  axc15  2444  sbimdvOLD  2516  sbimdOLD  2518  2eu6  2742  reuss2  4283  ssuni  4863  omordi  8192  nnawordi  8247  nnmordi  8257  omabs  8274  omsmolem  8280  alephordi  9500  dfac5  9554  dfac2a  9555  fin23lem14  9755  facdiv  13648  facwordi  13650  o1lo1  14894  rlimuni  14907  o1co  14943  rlimcn1  14945  rlimcn2  14947  rlimo1  14973  lo1add  14983  lo1mul  14984  rlimno1  15010  caucvgrlem  15029  caucvgrlem2  15031  gcdcllem1  15848  algcvgblem  15921  isprm5  16051  prmfac1  16063  infpnlem1  16246  gsummptnn0fz  19106  gsummoncoe1  20472  dmatscmcl  21112  decpmatmulsumfsupp  21381  pmatcollpw1lem1  21382  pmatcollpw2lem  21385  pmatcollpwfi  21390  pm2mpmhmlem1  21426  pm2mp  21433  cpmidpmatlem3  21480  cayhamlem4  21496  isclo2  21696  lmcls  21910  isnrm3  21967  dfconn2  22027  1stcrest  22061  dfac14lem  22225  cnpflf2  22608  isucn2  22888  cncfco  23515  ovolicc2lem3  24120  dyadmbllem  24200  itgcn  24443  aalioulem2  24922  aalioulem3  24923  ulmcn  24987  rlimcxp  25551  o1cxp  25552  chtppilimlem2  26050  chtppilim  26051  pthdlem1  27547  mdsymlem6  30185  crefss  31113  ss2mcls  32815  mclsax  32816  rdgprc  33039  nosupno  33203  nosupres  33207  bj-imim21  33886  bj-axtd  33928  bj-nfimt  33971  bj-nfdt  34030  bj-19.23t  34099  bj-19.36im  34100  rdgeqoa  34654  rdgssun  34662  wl-cbvmotv  34768  pclclN  37042  isnacs3  39327  syl5imp  40866  imbi12VD  41227  sbcim2gVD  41229  limsupre3lem  42033  limsupub2  42113  sgoldbeven3prm  43968  ply1mulgsumlem3  44462  ply1mulgsumlem4  44463