![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impr | GIF version |
Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Ref | Expression |
---|---|
impr.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
impr | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impr.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | |
2 | 1 | ex 114 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp32 254 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: reximddv2 2478 moi2 2797 preq12bg 3623 ordsuc 4392 f1ocnv2d 5862 supisoti 6759 caucvgsrlemoffres 7406 prodge0 8376 un0addcl 8767 un0mulcl 8768 peano2uz2 8914 elfz2nn0 9587 fzind2 9711 expaddzap 10060 expmulzap 10062 cau3lem 10608 climuni 10742 climrecvg1n 10798 fisumcom2 10893 dvdsval2 11138 algcvga 11372 lcmgcdlem 11398 divgcdcoprmex 11423 epttop 11851 |
Copyright terms: Public domain | W3C validator |