![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exp32 | GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp32.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
exp32 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp32.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
2 | 1 | ex 115 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
3 | 2 | expd 258 | 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-ia3 108 |
This theorem is referenced by: exp44 373 exp45 374 expr 375 anassrs 400 an13s 567 3impb 1199 xordidc 1399 f0rn0 5410 funfvima3 5750 isoini 5818 ovg 6012 fundmen 6805 distrlem1prl 7580 distrlem1pru 7581 caucvgprprlemaddq 7706 recexgt0sr 7771 axpre-suploclemres 7899 cnegexlem2 8131 mulgt1 8818 faclbnd 10716 divgcdcoprm0 12095 cncongr2 12098 oddpwdclemdvds 12164 oddpwdclemndvds 12165 infpnlem1 12351 cnpnei 13612 zabsle1 14293 |
Copyright terms: Public domain | W3C validator |