![]() |
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 1148 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp32 255 | 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: 3adant3r1 1158 3adant3r2 1159 3adant3r3 1160 3adant1l 1176 3adant1r 1177 mp3an1 1270 soinxp 4547 sotri 4870 fnfco 5233 mpoeq3dva 5767 fovrnda 5846 ovelrn 5851 grprinvd 5898 fnmpoovd 6042 nnmsucr 6314 fidifsnid 6694 exmidpw 6731 undiffi 6742 fidcenumlemim 6768 ltpopr 7304 ltexprlemdisj 7315 recexprlemdisj 7339 mul4 7765 add4 7794 2addsub 7847 addsubeq4 7848 subadd4 7877 muladd 8013 ltleadd 8075 divmulap 8296 divap0 8305 div23ap 8312 div12ap 8315 divsubdirap 8329 divcanap5 8335 divmuleqap 8338 divcanap6 8340 divdiv32ap 8341 div2subap 8457 letrp1 8464 lemul12b 8477 lediv1 8485 cju 8577 nndivre 8614 nndivtr 8620 nn0addge1 8875 nn0addge2 8876 peano2uz2 9010 uzind 9014 uzind3 9016 fzind 9018 fnn0ind 9019 uzind4 9233 qre 9267 irrmul 9289 rpdivcl 9316 rerpdivcl 9321 iccshftr 9618 iccshftl 9620 iccdil 9622 icccntr 9624 fzaddel 9680 fzrev 9705 frec2uzf1od 10020 expdivap 10185 2shfti 10444 iooinsup 10885 isermulc2 10948 dvds2add 11322 dvds2sub 11323 dvdstr 11325 alzdvds 11347 divalg2 11418 lcmgcdlem 11551 lcmgcdeq 11557 isprm6 11618 tgclb 12016 topbas 12018 neissex 12116 cnpnei 12169 txcnp 12221 psmetxrge0 12260 psmetlecl 12262 xmetlecl 12295 xmettpos 12298 elbl3ps 12322 elbl3 12323 metss 12422 comet 12427 bdxmet 12429 bdmet 12430 bl2ioo 12461 cncffvrn 12482 divccncfap 12490 |
Copyright terms: Public domain | W3C validator |