![]() |
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 115 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1193 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: mopick2 2109 3gencl 2773 mob2 2919 moi 2922 reupick3 3422 disjne 3478 disji2 3998 tz7.2 4356 funopg 5252 fvun1 5584 fvopab6 5614 isores3 5818 ovmpt4g 5999 ovmpos 6000 ov2gf 6001 ofrval 6095 poxp 6235 smoel 6303 tfr1onlemaccex 6351 tfrcllemaccex 6364 nnaass 6488 qsel 6614 xpdom3m 6836 phpm 6867 ctssdc 7114 mkvprop 7158 prarloclem3 7498 aptisr 7780 axpre-apti 7886 axapti 8030 addn0nid 8333 divvalap 8633 letrp1 8807 p1le 8808 zextle 9346 zextlt 9347 btwnnz 9349 gtndiv 9350 uzind2 9367 fzind 9370 iccleub 9933 uzsubsubfz 10049 elfz0fzfz0 10128 difelfznle 10137 elfzo0le 10187 fzonmapblen 10189 fzofzim 10190 fzosplitprm1 10236 rebtwn2zlemstep 10255 qbtwnxr 10260 icogelb 10268 expcl2lemap 10534 expclzaplem 10546 expnegzap 10556 leexp2r 10576 expnbnd 10646 bcval4 10734 bccmpl 10736 absexpzap 11091 divalgb 11932 ndvdssub 11937 dvdsgcd 12015 dfgcd2 12017 rplpwr 12030 nnmindc 12037 lcmgcdlem 12079 coprmdvds1 12093 qredeq 12098 prmdvdsexpr 12152 nnnn0modprm0 12257 pcexp 12311 difsqpwdvds 12339 prmpwdvds 12355 elrestr 12701 isnmgm 12784 grpasscan1 12938 grpinvnz 12946 mulgneg2 13022 dvdsrmul1 13276 dvdsunit 13286 lmodlema 13387 mopni 14067 sincosq1lem 14331 logbgcd1irr 14470 2lgsoddprmlem3 14544 |
Copyright terms: Public domain | W3C validator |