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 648 pm2.18dc 840 con4biddc 842 hbim1 1549 sbcof2 1782 ralimia 2493 ceqsalg 2714 rspct 2782 elabgt 2825 fvmptt 5512 ordiso2 6920 bj-exlimmp 12976 bj-rspgt 12993 bj-indint 13129 |
Copyright terms: Public domain | W3C validator |