![]() |
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 1148 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp31 254 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 930 |
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 932 |
This theorem is referenced by: ad4ant123 1161 ad4ant124 1162 ad4ant134 1163 ad4ant234 1164 3anidm23 1243 mp3an2 1271 mpd3an3 1284 rgen3 2478 moi2 2818 sbc3ie 2934 preq12bg 3647 issod 4179 wepo 4219 reuhypd 4330 funimass4 5404 fvtp1g 5560 f1imass 5607 fcof1o 5622 f1ofveu 5694 f1ocnvfv3 5695 acexmid 5705 2ndrn 6011 frecrdg 6235 oawordriexmid 6296 mapxpen 6671 findcard 6711 findcard2 6712 findcard2s 6713 ltapig 7047 ltanqi 7111 ltmnqi 7112 lt2addnq 7113 lt2mulnq 7114 prarloclemcalc 7211 genpassl 7233 genpassu 7234 prmuloc 7275 ltexprlemm 7309 ltexprlemfl 7318 ltexprlemfu 7320 lteupri 7326 ltaprg 7328 mul4 7765 add4 7794 cnegexlem2 7809 cnegexlem3 7810 2addsub 7847 addsubeq4 7848 muladd 8013 ltleadd 8075 reapmul1 8223 apreim 8231 receuap 8291 p1le 8465 lemul12b 8477 lbinf 8564 zdiv 8991 fzind 9018 fnn0ind 9019 uzss 9196 qmulcl 9279 qreccl 9284 xrlttr 9422 xaddass 9493 icc0r 9550 iooshf 9576 elfz5 9639 elfz0fzfz0 9744 fzind2 9857 ioo0 9878 ico0 9880 ioc0 9881 expnegap0 10142 expineg2 10143 mulexpzap 10174 expsubap 10182 expnbnd 10256 facndiv 10326 bccmpl 10341 bcval5 10350 bcpasc 10353 crim 10471 climshftlemg 10910 2sumeq2dv 10979 hash2iun 11087 dvdsval3 11292 dvdsnegb 11305 muldvds1 11313 muldvds2 11314 dvdscmul 11315 dvdsmulc 11316 dvds2ln 11321 divalgb 11417 ndvdssub 11422 gcddiv 11500 rpexp1i 11625 phiprmpw 11690 hashgcdeq 11696 innei 12114 iscnp4 12168 cnpnei 12169 cnnei 12182 cnconst 12184 ismeti 12274 isxmet2d 12276 elbl2ps 12320 elbl2 12321 xblpnfps 12326 xblpnf 12327 xblm 12345 blininf 12352 blssexps 12357 blssex 12358 blsscls2 12421 metss 12422 metrest 12434 metcn 12438 cdivcncfap 12499 |
Copyright terms: Public domain | W3C validator |