![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3expb | GIF version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3expb | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3exp 1204 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp32 257 | 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: 3adant3r1 1214 3adant3r2 1215 3adant3r3 1216 3adant1l 1232 3adant1r 1233 mp3an1 1335 soinxp 4714 sotri 5042 fnfco 5409 mpoeq3dva 5959 fovcdmda 6039 ovelrn 6044 fnmpoovd 6239 nnmsucr 6512 fidifsnid 6898 exmidpw 6935 undiffi 6952 fidcenumlemim 6980 ltpopr 7623 ltexprlemdisj 7634 recexprlemdisj 7658 mul4 8118 add4 8147 2addsub 8200 addsubeq4 8201 subadd4 8230 muladd 8370 ltleadd 8432 divmulap 8661 divap0 8670 div23ap 8677 div12ap 8680 divsubdirap 8694 divcanap5 8700 divmuleqap 8703 divcanap6 8705 divdiv32ap 8706 div2subap 8823 letrp1 8834 lemul12b 8847 lediv1 8855 cju 8947 nndivre 8984 nndivtr 8990 nn0addge1 9251 nn0addge2 9252 peano2uz2 9389 uzind 9393 uzind3 9395 fzind 9397 fnn0ind 9398 uzind4 9617 qre 9654 irrmul 9676 rpdivcl 9708 rerpdivcl 9713 iccshftr 10023 iccshftl 10025 iccdil 10027 icccntr 10029 fzaddel 10088 fzrev 10113 frec2uzf1od 10436 expdivap 10601 2shfti 10871 iooinsup 11316 isermulc2 11379 dvds2add 11863 dvds2sub 11864 dvdstr 11866 alzdvds 11891 divalg2 11962 lcmgcdlem 12108 lcmgcdeq 12114 isprm6 12178 pcqcl 12337 mgmplusf 12839 grpinva 12859 ismndd 12895 idmhm 12918 issubm2 12922 submid 12926 0mhm 12935 resmhm 12936 resmhm2 12937 resmhm2b 12938 mhmco 12939 mhmima 12940 grpinvcnv 13009 grpinvnzcl 13013 grpsubf 13020 imasgrp2 13049 qusgrp2 13052 mhmfmhm 13056 mulgnnsubcl 13071 mulgnn0z 13086 mulgnndir 13088 issubg4m 13129 isnsg3 13143 nsgid 13151 qusadd 13170 ghmmhm 13189 ghmmhmb 13190 idghm 13195 resghm 13196 ghmf1 13209 kerf1ghm 13210 qusghm 13218 ablnsg 13268 srgfcl 13324 srgmulgass 13340 srglmhm 13344 srgrmhm 13345 opprringbg 13427 mulgass3 13432 subrngringnsg 13549 issubrng2 13554 issubrg2 13585 islmodd 13606 lmodscaf 13623 lcomf 13640 rmodislmodlem 13663 issubrgd 13765 qusmul2 13840 crngridl 13841 qusmulrng 13843 tgclb 14017 topbas 14019 neissex 14117 cnpnei 14171 txcnp 14223 psmetxrge0 14284 psmetlecl 14286 xmetlecl 14319 xmettpos 14322 elbl3ps 14346 elbl3 14347 metss 14446 comet 14451 bdxmet 14453 bdmet 14454 bl2ioo 14494 divcnap 14507 cncfcdm 14521 divccncfap 14529 dvrecap 14629 cosz12 14653 |
Copyright terms: Public domain | W3C validator |