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 ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

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  55  embantd  56  imim12d  74  anc2r  326  pm5.31  345  con4biddc  842  jaddc  849  hbimd  1552  19.21ht  1560  nfimd  1564  19.23t  1655  spimth  1713  ssuni  3758  nnmordi  6412  omnimkv  7030  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  facdiv  10484  facwordi  10486  bezoutlemmain  11686  bezoutlemaz  11691  bezoutlembz  11692  algcvgblem  11730  prmfac1  11830  cncfco  12747  limccnpcntop  12813  limccoap  12816  bj-rspgt  12993