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 633 pm2.18dc 825 con4biddc 827 hbim1 1534 sbcof2 1766 ralimia 2470 ceqsalg 2688 rspct 2756 elabgt 2799 fvmptt 5480 ordiso2 6888 bj-exlimmp 12903 bj-rspgt 12920 bj-indint 13056 |
Copyright terms: Public domain | W3C validator |