Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3expa | GIF version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3expa | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3exp 1103 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp31 243 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∧ w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: 3anidm23 1194 mp3an2 1220 mpd3an3 1233 rgen3 2406 moi2 2722 sbc3ie 2831 preq12bg 3544 issod 4056 wepo 4096 reuhypd 4203 funimass4 5224 fvtp1g 5369 f1imass 5413 fcof1o 5429 f1ofveu 5500 f1ocnvfv3 5501 acexmid 5511 2ndrn 5809 rdgon 5973 frecrdg 5992 findcard 6345 findcard2 6346 findcard2s 6347 ltapig 6436 ltanqi 6500 ltmnqi 6501 lt2addnq 6502 lt2mulnq 6503 prarloclemcalc 6600 genpassl 6622 genpassu 6623 prmuloc 6664 ltexprlemm 6698 ltexprlemfl 6707 ltexprlemfu 6709 lteupri 6715 ltaprg 6717 mul4 7145 add4 7172 cnegexlem2 7187 cnegexlem3 7188 2addsub 7225 addsubeq4 7226 muladd 7381 ltleadd 7441 reapmul1 7586 apreim 7594 receuap 7650 p1le 7815 lemul12b 7827 zdiv 8328 fzind 8353 fnn0ind 8354 uzss 8493 qmulcl 8572 qreccl 8576 xrlttr 8716 icc0r 8795 iooshf 8821 elfz5 8882 elfz0fzfz0 8983 fzind2 9095 expnegap0 9263 expineg2 9264 mulexpzap 9295 expsubap 9302 expnbnd 9372 crim 9458 climshftlemg 9823 |
Copyright terms: Public domain | W3C validator |