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 326 pm5.31 346 con4biddc 847 jaddc 854 hbimd 1560 19.21ht 1568 nfimd 1572 19.23t 1664 spimth 1722 ssuni 3805 nnmordi 6475 omnimkv 7111 caucvgsrlemoffcau 7730 caucvgsrlemoffres 7732 facdiv 10640 facwordi 10642 bezoutlemmain 11916 bezoutlemaz 11921 bezoutlembz 11922 algcvgblem 11960 prmfac1 12061 cncfco 13119 limccnpcntop 13185 limccoap 13188 bj-rspgt 13502 |
Copyright terms: Public domain | W3C validator |