Theorem imim2d 55

Description: Deduction adding nested antecedents. Deduction associated with imim2 56 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  56  embantd  57  imim12d  79  anc2r  577  pm5.31  610  dedlem0b  992  nic-ax  1589  nic-axALT  1590  sylgt  1739  nfimdOLD  2214  2eu6  2546  reuss2  3866  ssuni  4395  ssuniOLD  4396  omordi  7533  nnawordi  7588  nnmordi  7598  omabs  7614  omsmolem  7620  alephordi  8780  dfac5  8834  dfac2a  8835  fin23lem14  9038  facdiv  12936  facwordi  12938  o1lo1  14116  rlimuni  14129  o1co  14165  rlimcn1  14167  rlimcn2  14169  rlimo1  14195  lo1add  14205  lo1mul  14206  rlimno1  14232  caucvgrlem  14251  caucvgrlem2  14253  gcdcllem1  15059  algcvgblem  15128  isprm5  15257  prmfac1  15269  infpnlem1  15452  gsummptnn0fz  18205  gsummoncoe1  19495  dmatscmcl  20128  decpmatmulsumfsupp  20397  pmatcollpw1lem1  20398  pmatcollpw2lem  20401  pmatcollpwfi  20406  pm2mpmhmlem1  20442  pm2mp  20449  cpmidpmatlem3  20496  cayhamlem4  20512  isclo2  20702  lmcls  20916  isnrm3  20973  dfcon2  21032  1stcrest  21066  dfac14lem  21230  cnpflf2  21614  isucn2  21893  cncfco  22518  ovolicc2lem3  23094  dyadmbllem  23173  itgcn  23415  aalioulem2  23892  aalioulem3  23893  ulmcn  23957  rlimcxp  24500  o1cxp  24501  chtppilimlem2  24963  chtppilim  24964  frgrancvvdgeq  26570  mdsymlem6  28651  crefss  29244  ss2mcls  30719  mclsax  30720  rdgprc  30944  bj-imim21  31709  bj-axtd  31751  bj-ssbim  31810  bj-nfdt  31873  bj-nfimt  32025  rdgeqoa  32394  pm5.31r  33159  pclclN  34195  isnacs3  36291  syl5imp  37739  imbi12VD  38131  sbcim2gVD  38133  pthdlem1  40972  ply1mulgsumlem3  41970  ply1mulgsumlem4  41971