![]() |
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 1181 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp32 255 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 3adant3r1 1191 3adant3r2 1192 3adant3r3 1193 3adant1l 1209 3adant1r 1210 mp3an1 1303 soinxp 4617 sotri 4942 fnfco 5305 mpoeq3dva 5843 fovrnda 5922 ovelrn 5927 grprinvd 5974 fnmpoovd 6120 nnmsucr 6392 fidifsnid 6773 exmidpw 6810 undiffi 6821 fidcenumlemim 6848 ltpopr 7427 ltexprlemdisj 7438 recexprlemdisj 7462 mul4 7918 add4 7947 2addsub 8000 addsubeq4 8001 subadd4 8030 muladd 8170 ltleadd 8232 divmulap 8459 divap0 8468 div23ap 8475 div12ap 8478 divsubdirap 8492 divcanap5 8498 divmuleqap 8501 divcanap6 8503 divdiv32ap 8504 div2subap 8620 letrp1 8630 lemul12b 8643 lediv1 8651 cju 8743 nndivre 8780 nndivtr 8786 nn0addge1 9047 nn0addge2 9048 peano2uz2 9182 uzind 9186 uzind3 9188 fzind 9190 fnn0ind 9191 uzind4 9410 qre 9444 irrmul 9466 rpdivcl 9496 rerpdivcl 9501 iccshftr 9807 iccshftl 9809 iccdil 9811 icccntr 9813 fzaddel 9870 fzrev 9895 frec2uzf1od 10210 expdivap 10375 2shfti 10635 iooinsup 11078 isermulc2 11141 dvds2add 11563 dvds2sub 11564 dvdstr 11566 alzdvds 11588 divalg2 11659 lcmgcdlem 11794 lcmgcdeq 11800 isprm6 11861 tgclb 12273 topbas 12275 neissex 12373 cnpnei 12427 txcnp 12479 psmetxrge0 12540 psmetlecl 12542 xmetlecl 12575 xmettpos 12578 elbl3ps 12602 elbl3 12603 metss 12702 comet 12707 bdxmet 12709 bdmet 12710 bl2ioo 12750 divcnap 12763 cncffvrn 12777 divccncfap 12785 dvrecap 12885 cosz12 12909 |
Copyright terms: Public domain | W3C validator |