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 1160 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: mopick2 2060 3gencl 2694 mob2 2837 moi 2840 reupick3 3331 disjne 3386 disji2 3892 tz7.2 4246 funopg 5127 fvun1 5455 fvopab6 5485 isores3 5684 ovmpt4g 5861 ovmpos 5862 ov2gf 5863 ofrval 5960 poxp 6097 smoel 6165 tfr1onlemaccex 6213 tfrcllemaccex 6226 nnaass 6349 qsel 6474 xpdom3m 6696 phpm 6727 ctssdc 6966 mkvprop 7000 prarloclem3 7273 aptisr 7555 axpre-apti 7661 axapti 7803 addn0nid 8104 divvalap 8402 letrp1 8574 p1le 8575 zextle 9110 zextlt 9111 btwnnz 9113 gtndiv 9114 uzind2 9131 fzind 9134 iccleub 9682 uzsubsubfz 9795 elfz0fzfz0 9871 difelfznle 9880 elfzo0le 9930 fzonmapblen 9932 fzofzim 9933 fzosplitprm1 9979 rebtwn2zlemstep 9998 qbtwnxr 10003 expcl2lemap 10273 expclzaplem 10285 expnegzap 10295 leexp2r 10315 expnbnd 10383 bcval4 10466 bccmpl 10468 absexpzap 10820 divalgb 11549 ndvdssub 11554 dvdsgcd 11627 dfgcd2 11629 rplpwr 11642 lcmgcdlem 11685 coprmdvds1 11699 qredeq 11704 prmdvdsexpr 11755 elrestr 12055 mopni 12578 sincosq1lem 12833 |
Copyright terms: Public domain | W3C validator |