![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3expib | GIF version |
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3expib | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3exp 1143 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 252 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 925 |
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 depends on definitions: df-bi 116 df-3an 927 |
This theorem is referenced by: 3anidm12 1232 mob 2798 eqbrrdva 4619 funimaexglem 5110 fco 5189 f1oiso2 5620 caovimo 5852 smoel2 6082 nnaword 6284 3ecoptocl 6395 sbthlemi10 6729 distrnq0 7072 addassnq0 7075 prcdnql 7097 prcunqu 7098 genpdisj 7136 cauappcvgprlemrnd 7263 caucvgprlemrnd 7286 caucvgprprlemrnd 7314 nn0n0n1ge2b 8880 fzind 8915 icoshft 9461 fzen 9511 iseqcoll 10301 shftuz 10305 mulgcd 11337 algcvga 11365 lcmneg 11388 |
Copyright terms: Public domain | W3C validator |