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 114 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
3 | 2 | expd 256 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: exp44 370 exp45 371 expr 372 anassrs 397 an13s 556 3impb 1177 xordidc 1377 f0rn0 5312 funfvima3 5644 isoini 5712 ovg 5902 fundmen 6693 distrlem1prl 7383 distrlem1pru 7384 caucvgprprlemaddq 7509 recexgt0sr 7574 axpre-suploclemres 7702 cnegexlem2 7931 mulgt1 8614 faclbnd 10480 divgcdcoprm0 11771 cncongr2 11774 oddpwdclemdvds 11837 oddpwdclemndvds 11838 cnpnei 12377 |
Copyright terms: Public domain | W3C validator |