![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imim2d | GIF version |
Description: Deduction adding nested antecedents. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imim2d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
imim2d | ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim2d.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | a1d 22 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒))) |
3 | 2 | a2d 26 | 1 ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒))) |
Colors of variables: wff set class |
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 328 pm5.31 348 con4biddc 858 jaddc 865 hbimd 1584 19.21ht 1592 nfimd 1596 19.23t 1688 spimth 1746 ssuni 3846 nnmordi 6536 omnimkv 7179 caucvgsrlemoffcau 7822 caucvgsrlemoffres 7824 facdiv 10745 facwordi 10747 bezoutlemmain 12026 bezoutlemaz 12031 bezoutlembz 12032 algcvgblem 12076 prmfac1 12179 infpnlem1 12386 cncfco 14515 limccnpcntop 14581 limccoap 14584 bj-rspgt 14975 |
Copyright terms: Public domain | W3C validator |