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-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: expdimp 257 pm3.3 259 syland 291 exp32 363 exp4c 366 exp4d 367 exp42 369 exp44 371 exp5c 374 impl 378 mpan2d 426 a2and 553 pm2.6dc 857 3impib 1196 exp5o 1221 biassdc 1390 exbir 1429 expcomd 1434 expdcom 1435 mopick 2097 ralrimivv 2551 mob2 2910 reuind 2935 difin 3364 reupick3 3412 suctr 4406 tfisi 4571 relop 4761 funcnvuni 5267 fnun 5304 mpteqb 5586 funfvima 5727 poxp 6211 nnmass 6466 supisoti 6987 axprecex 7842 ltnsym 8005 nn0lt2 9293 fzind 9327 fnn0ind 9328 btwnz 9331 lbzbi 9575 ledivge1le 9683 elfz0ubfz0 10081 elfzo0z 10140 fzofzim 10144 flqeqceilz 10274 leexp2r 10530 bernneq 10596 cau3lem 11078 climuni 11256 mulcn2 11275 dvdsabseq 11807 ndvdssub 11889 bezoutlemmain 11953 rplpwr 11982 algcvgblem 12003 euclemma 12100 insubm 12703 grpinveu 12741 basis2 12840 txcnp 13065 metcnp3 13305 bj-charfunr 13845 |
Copyright terms: Public domain | W3C validator |