Theorem imim2d 54

Description: Deduction adding nested antecedents. (Contributed by NM, 5-Aug-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 22	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3	2	a2d 26	1 ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim2  55  embantd  56  imim12d  74  anc2r  328  pm5.31  348  con4biddc  869  jaddc  876  hbimd  1626  19.21ht  1634  nfimd  1638  19.23t  1729  spimth  1788  ssuni  3957  nnmordi  6789  omnimkv  7496  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  facdiv  11178  facwordi  11180  bezoutlemmain  12777  bezoutlemaz  12782  bezoutlembz  12783  algcvgblem  12829  prmfac1  12932  infpnlem1  13140  mplsubgfileminv  15093  cncfco  15694  limccnpcntop  15778  limccoap  15781  bj-rspgt  16826