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 1137 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp32 253 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 919 |
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 921 |
This theorem is referenced by: 3adant3r1 1147 3adant3r2 1148 3adant3r3 1149 3adant1l 1161 3adant1r 1162 mp3an1 1255 soinxp 4428 sotri 4740 fnfco 5085 mpt2eq3dva 5589 fovrnda 5664 ovelrn 5669 grprinvd 5716 nnmsucr 6090 ltpopr 6785 ltexprlemdisj 6796 recexprlemdisj 6820 mul4 7240 add4 7269 2addsub 7322 addsubeq4 7323 subadd4 7352 muladd 7488 ltleadd 7550 divmulap 7763 divap0 7772 div23ap 7779 div12ap 7782 divsubdirap 7796 divcanap5 7802 divmuleqap 7805 divcanap6 7807 divdiv32ap 7808 letrp1 7926 lemul12b 7939 lediv1 7947 cju 8038 nndivre 8074 nndivtr 8080 nn0addge1 8334 nn0addge2 8335 peano2uz2 8454 uzind 8458 uzind3 8460 fzind 8462 fnn0ind 8463 uzind4 8676 qre 8710 irrmul 8732 rpdivcl 8759 rerpdivcl 8764 iccshftr 9016 iccshftl 9018 iccdil 9020 icccntr 9022 fzaddel 9077 fzrev 9101 frec2uzf1od 9408 expdivap 9527 2shfti 9719 iisermulc2 10178 dvds2add 10229 dvds2sub 10230 dvdstr 10232 alzdvds 10254 divalg2 10326 lcmgcdlem 10459 lcmgcdeq 10465 isprm6 10526 |
Copyright terms: Public domain | W3C validator |