![]() |
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 115 | . 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
4 | 3 | com3r 79 | 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: expdimp 259 pm3.3 261 syland 293 exp32 365 exp4c 368 exp4d 369 exp42 371 exp44 373 exp5c 376 impl 380 mpan2d 428 a2and 558 pm2.6dc 863 3impib 1202 exp5o 1227 biassdc 1405 exbir 1446 expcomd 1451 expdcom 1452 mopick 2114 ralrimivv 2568 mob2 2929 reuind 2954 difin 3384 reupick3 3432 suctr 4433 tfisi 4598 relop 4789 funcnvuni 5297 fnun 5334 mpteqb 5619 funfvima 5761 poxp 6246 nnmass 6501 supisoti 7022 axprecex 7892 ltnsym 8056 nn0lt2 9347 fzind 9381 fnn0ind 9382 btwnz 9385 lbzbi 9629 ledivge1le 9739 elfz0ubfz0 10138 elfzo0z 10197 fzofzim 10201 flqeqceilz 10331 leexp2r 10587 bernneq 10654 cau3lem 11136 climuni 11314 mulcn2 11333 dvdsabseq 11866 ndvdssub 11948 bezoutlemmain 12012 rplpwr 12041 algcvgblem 12062 euclemma 12159 insubm 12893 grpinveu 12934 srgmulgass 13236 basis2 13819 txcnp 14042 metcnp3 14282 bj-charfunr 14833 |
Copyright terms: Public domain | W3C validator |