![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expd | GIF version |
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.) |
Ref | Expression |
---|---|
exp3a.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Ref | Expression |
---|---|
expd | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp3a.1 | . . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
2 | 1 | com12 30 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃)) |
3 | 2 | ex 114 | . 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
4 | 3 | com3r 79 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 |
This theorem is referenced by: expdimp 256 pm3.3 258 syland 288 exp32 358 exp4c 361 exp4d 362 exp42 364 exp44 366 exp5c 369 impl 373 mpan2d 420 a2and 526 pm2.6dc 798 3impib 1142 exp5o 1163 biassdc 1332 exbir 1371 expcomd 1376 expdcom 1377 mopick 2027 ralrimivv 2455 mob2 2796 reuind 2821 difin 3237 reupick3 3285 suctr 4257 tfisi 4415 relop 4599 funcnvuni 5096 fnun 5133 mpteqb 5406 funfvima 5540 poxp 6011 nnmass 6262 supisoti 6759 axprecex 7476 ltnsym 7632 nn0lt2 8889 fzind 8922 fnn0ind 8923 btwnz 8926 lbzbi 9162 ledivge1le 9264 elfz0ubfz0 9597 elfzo0z 9656 fzofzim 9660 flqeqceilz 9786 leexp2r 10070 bernneq 10135 cau3lem 10608 climuni 10742 mulcn2 10762 dvdsabseq 11187 ndvdssub 11269 bezoutlemmain 11326 rplpwr 11355 algcvgblem 11370 euclemma 11464 basis2 11807 |
Copyright terms: Public domain | W3C validator |