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 371 exp45 372 expr 373 anassrs 398 an13s 557 3impb 1181 xordidc 1381 f0rn0 5363 funfvima3 5697 isoini 5765 ovg 5956 fundmen 6748 distrlem1prl 7497 distrlem1pru 7498 caucvgprprlemaddq 7623 recexgt0sr 7688 axpre-suploclemres 7816 cnegexlem2 8046 mulgt1 8729 faclbnd 10610 divgcdcoprm0 11972 cncongr2 11975 oddpwdclemdvds 12039 oddpwdclemndvds 12040 cnpnei 12606 |
Copyright terms: Public domain | W3C validator |