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 23 | 1 ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: imim2 49 embantd 50 imim12d 68 anc2r 311 pm5.31 330 con4biddc 754 jaddc 761 hbimd 1465 19.21ht 1473 nfimd 1477 19.23t 1567 spimth 1623 ssuni 3602 nnmordi 6089 caucvgsrlemoffcau 6882 caucvgsrlemoffres 6884 algcvgblem 9888 bj-rspgt 9925 |
Copyright terms: Public domain | W3C validator |