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 316 ancr 319 anc2r 326 pm2.65 649 pm2.18dc 845 con4biddc 847 hbim1 1557 sbcof2 1797 ralimia 2525 ceqsalg 2749 rspct 2818 elabgt 2862 fvmptt 5571 ordiso2 6991 bj-exlimmp 13491 bj-rspgt 13508 bj-indint 13654 |
Copyright terms: Public domain | W3C validator |