![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3impia | GIF version |
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Ref | Expression |
---|---|
3impia.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
3impia | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impia.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | |
2 | 1 | ex 114 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1138 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 925 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 927 |
This theorem is referenced by: mopick2 2032 3gencl 2654 mob2 2796 moi 2799 reupick3 3285 disjne 3340 disji2 3844 tz7.2 4190 funopg 5061 fvun1 5383 fvopab6 5410 isores3 5608 ovmpt4g 5781 ovmpt2s 5782 ov2gf 5783 ofrval 5880 poxp 6011 smoel 6079 tfr1onlemaccex 6127 tfrcllemaccex 6140 nnaass 6260 qsel 6383 xpdom3m 6604 phpm 6635 prarloclem3 7117 aptisr 7385 axpre-apti 7481 axapti 7618 addn0nid 7913 divvalap 8202 letrp1 8370 p1le 8371 zextle 8898 zextlt 8899 btwnnz 8901 gtndiv 8902 uzind2 8919 fzind 8922 iccleub 9410 uzsubsubfz 9522 elfz0fzfz0 9598 difelfznle 9607 elfzo0le 9657 fzonmapblen 9659 fzofzim 9660 fzosplitprm1 9706 rebtwn2zlemstep 9725 qbtwnxr 9730 expcl2lemap 10028 expclzaplem 10040 expnegzap 10050 leexp2r 10070 expnbnd 10138 bcval4 10221 bccmpl 10223 absexpzap 10574 divalgb 11264 ndvdssub 11269 dvdsgcd 11340 dfgcd2 11342 rplpwr 11355 lcmgcdlem 11398 coprmdvds1 11412 qredeq 11417 prmdvdsexpr 11468 elrestr 11721 |
Copyright terms: Public domain | W3C validator |