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 562 3impb 1194 xordidc 1394 f0rn0 5392 funfvima3 5729 isoini 5797 ovg 5991 fundmen 6784 distrlem1prl 7544 distrlem1pru 7545 caucvgprprlemaddq 7670 recexgt0sr 7735 axpre-suploclemres 7863 cnegexlem2 8095 mulgt1 8779 faclbnd 10675 divgcdcoprm0 12055 cncongr2 12058 oddpwdclemdvds 12124 oddpwdclemndvds 12125 infpnlem1 12311 cnpnei 13013 zabsle1 13694 |
Copyright terms: Public domain | W3C validator |