![]() |
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 1204 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp31 256 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 |
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 982 |
This theorem is referenced by: ad4ant123 1217 ad4ant124 1218 ad4ant134 1219 ad4ant234 1220 ad5ant123 1241 3anidm23 1308 mp3an2 1336 mpd3an3 1349 rgen3 2577 moi2 2933 sbc3ie 3051 preq12bg 3788 issod 4337 wepo 4377 reuhypd 4489 funimass4 5587 fvtp1g 5745 f1imass 5796 fcof1o 5811 f1ofveu 5885 f1ocnvfv3 5886 acexmid 5896 2ndrn 6209 frecrdg 6434 oawordriexmid 6496 mapxpen 6877 findcard 6917 findcard2 6918 findcard2s 6919 ltapig 7368 ltanqi 7432 ltmnqi 7433 lt2addnq 7434 lt2mulnq 7435 prarloclemcalc 7532 genpassl 7554 genpassu 7555 prmuloc 7596 ltexprlemm 7630 ltexprlemfl 7639 ltexprlemfu 7641 lteupri 7647 ltaprg 7649 mul4 8120 add4 8149 cnegexlem2 8164 cnegexlem3 8165 2addsub 8202 addsubeq4 8203 muladd 8372 ltleadd 8434 reapmul1 8583 apreim 8591 receuap 8657 p1le 8837 lemul12b 8849 lbinf 8936 zdiv 9372 fzind 9399 fnn0ind 9400 uzss 9580 qmulcl 9669 qreccl 9674 xrlttr 9827 xaddass 9901 icc0r 9958 iooshf 9984 elfz5 10049 elfz0fzfz0 10158 fzind2 10271 ioo0 10292 ico0 10294 ioc0 10295 expnegap0 10562 expineg2 10563 mulexpzap 10594 expsubap 10602 expnbnd 10678 facndiv 10754 bccmpl 10769 bcval5 10778 bcpasc 10781 crim 10902 climshftlemg 11345 2sumeq2dv 11414 hash2iun 11522 2cprodeq2dv 11611 dvdsval3 11833 dvdsnegb 11850 muldvds1 11858 muldvds2 11859 dvdscmul 11860 dvdsmulc 11861 dvds2ln 11866 divalgb 11965 ndvdssub 11970 gcddiv 12055 rpexp1i 12189 phiprmpw 12257 hashgcdeq 12274 pythagtriplem1 12300 pockthg 12392 infpnlem1 12394 4sqlem3 12425 imasaddfnlemg 12794 mndpfo 12914 grplmulf1o 13033 grplactcnv 13061 mulgnn0subcl 13092 mulgsubcl 13093 mulgdir 13111 issubg2m 13145 issubgrpd2 13146 nmzsubg 13166 eqgen 13183 ghmmulg 13212 ghmf1 13229 kerf1ghm 13230 conjghm 13232 srglmhm 13364 srgrmhm 13365 oppr1g 13449 dvdsrcl2 13466 crngunit 13478 subsubrng 13578 subrgugrp 13604 subsubrg 13609 islmod 13624 lmodvsdir 13645 lmodvsass 13646 lsssubg 13710 lss1d 13716 lidlsubg 13819 lidlsubcl 13820 mulgghm2 13923 innei 14140 iscnp4 14195 cnpnei 14196 cnnei 14209 cnconst 14211 ismeti 14323 isxmet2d 14325 elbl2ps 14369 elbl2 14370 xblpnfps 14375 xblpnf 14376 xblm 14394 blininf 14401 blssexps 14406 blssex 14407 blsscls2 14470 metss 14471 metrest 14483 metcn 14491 divcnap 14532 cdivcncfap 14564 lgslem4 14882 lgscllem 14886 lgsneg1 14904 lgsne0 14917 |
Copyright terms: Public domain | W3C validator |