![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > a2i | GIF version |
Description: Inference derived from Axiom ax-2 7. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
a2i.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
a2i | ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a2i.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | ax-2 7 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-2 7 |
This theorem is referenced by: imim2i 12 mpd 13 sylcom 28 pm2.43 53 ancl 318 ancr 321 anc2r 328 pm2.65 660 pm2.18dc 856 con4biddc 858 hbim1 1581 sbcof2 1821 ralimia 2551 ceqsalg 2784 rspct 2853 elabgt 2897 fvmptt 5637 ordiso2 7080 bj-exlimmp 15185 bj-rspgt 15202 bj-indint 15347 |
Copyright terms: Public domain | W3C validator |