![]() |
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 115 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp32 257 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: reximddv2 2582 moi2 2918 preq12bg 3771 ordsuc 4559 f1ocnv2d 6069 supisoti 7003 caucvgsrlemoffres 7787 prodge0 8797 un0addcl 9195 un0mulcl 9196 peano2uz2 9346 elfz2nn0 10095 fzind2 10222 expaddzap 10547 expmulzap 10549 cau3lem 11104 climuni 11282 climrecvg1n 11337 fisumcom2 11427 fprodcom2fi 11615 dvdsval2 11778 algcvga 12031 lcmgcdlem 12057 divgcdcoprmex 12082 prmpwdvds 12333 isgrpinv 12813 dvdsrcl2 13090 epttop 13254 cncnp 13394 cnconst 13398 bl2in 13567 metcnpi 13679 metcnpi2 13680 metcnpi3 13681 |
Copyright terms: Public domain | W3C validator |