![]() |
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 1138 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp32 253 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: 3adant3r1 1148 3adant3r2 1149 3adant3r3 1150 3adant1l 1162 3adant1r 1163 mp3an1 1256 soinxp 4430 sotri 4744 fnfco 5090 mpt2eq3dva 5594 fovrnda 5669 ovelrn 5674 grprinvd 5721 nnmsucr 6125 ltpopr 6836 ltexprlemdisj 6847 recexprlemdisj 6871 mul4 7296 add4 7325 2addsub 7378 addsubeq4 7379 subadd4 7408 muladd 7544 ltleadd 7606 divmulap 7819 divap0 7828 div23ap 7835 div12ap 7838 divsubdirap 7852 divcanap5 7858 divmuleqap 7861 divcanap6 7863 divdiv32ap 7864 letrp1 7982 lemul12b 7995 lediv1 8003 cju 8094 nndivre 8130 nndivtr 8136 nn0addge1 8390 nn0addge2 8391 peano2uz2 8524 uzind 8528 uzind3 8530 fzind 8532 fnn0ind 8533 uzind4 8746 qre 8780 irrmul 8802 rpdivcl 8829 rerpdivcl 8834 iccshftr 9081 iccshftl 9083 iccdil 9085 icccntr 9087 fzaddel 9142 fzrev 9166 frec2uzf1od 9477 expdivap 9613 2shfti 9846 iisermulc2 10305 dvds2add 10363 dvds2sub 10364 dvdstr 10366 alzdvds 10388 divalg2 10459 lcmgcdlem 10592 lcmgcdeq 10598 isprm6 10659 |
Copyright terms: Public domain | W3C validator |